Step 
Hyp 
Ref 
Expression 
1 

dfxpc 
 Xc. = ( r e. _V , s e. _V > [_ ( ( Base ` r ) X. ( Base ` s ) ) / b ]_ [_ ( u e. b , v e. b > ( ( ( 1st ` u ) ( Hom ` r ) ( 1st ` v ) ) X. ( ( 2nd ` u ) ( Hom ` s ) ( 2nd ` v ) ) ) ) / h ]_ { <. ( Base ` ndx ) , b >. , <. ( Hom ` ndx ) , h >. , <. ( comp ` ndx ) , ( x e. ( b X. b ) , y e. b > ( g e. ( ( 2nd ` x ) h y ) , f e. ( h ` x ) > <. ( ( 1st ` g ) ( <. ( 1st ` ( 1st ` x ) ) , ( 1st ` ( 2nd ` x ) ) >. ( comp ` r ) ( 1st ` y ) ) ( 1st ` f ) ) , ( ( 2nd ` g ) ( <. ( 2nd ` ( 1st ` x ) ) , ( 2nd ` ( 2nd ` x ) ) >. ( comp ` s ) ( 2nd ` y ) ) ( 2nd ` f ) ) >. ) ) >. } ) 
2 

tpex 
 { <. ( Base ` ndx ) , b >. , <. ( Hom ` ndx ) , h >. , <. ( comp ` ndx ) , ( x e. ( b X. b ) , y e. b > ( g e. ( ( 2nd ` x ) h y ) , f e. ( h ` x ) > <. ( ( 1st ` g ) ( <. ( 1st ` ( 1st ` x ) ) , ( 1st ` ( 2nd ` x ) ) >. ( comp ` r ) ( 1st ` y ) ) ( 1st ` f ) ) , ( ( 2nd ` g ) ( <. ( 2nd ` ( 1st ` x ) ) , ( 2nd ` ( 2nd ` x ) ) >. ( comp ` s ) ( 2nd ` y ) ) ( 2nd ` f ) ) >. ) ) >. } e. _V 
3 
2

csbex 
 [_ ( u e. b , v e. b > ( ( ( 1st ` u ) ( Hom ` r ) ( 1st ` v ) ) X. ( ( 2nd ` u ) ( Hom ` s ) ( 2nd ` v ) ) ) ) / h ]_ { <. ( Base ` ndx ) , b >. , <. ( Hom ` ndx ) , h >. , <. ( comp ` ndx ) , ( x e. ( b X. b ) , y e. b > ( g e. ( ( 2nd ` x ) h y ) , f e. ( h ` x ) > <. ( ( 1st ` g ) ( <. ( 1st ` ( 1st ` x ) ) , ( 1st ` ( 2nd ` x ) ) >. ( comp ` r ) ( 1st ` y ) ) ( 1st ` f ) ) , ( ( 2nd ` g ) ( <. ( 2nd ` ( 1st ` x ) ) , ( 2nd ` ( 2nd ` x ) ) >. ( comp ` s ) ( 2nd ` y ) ) ( 2nd ` f ) ) >. ) ) >. } e. _V 
4 
3

csbex 
 [_ ( ( Base ` r ) X. ( Base ` s ) ) / b ]_ [_ ( u e. b , v e. b > ( ( ( 1st ` u ) ( Hom ` r ) ( 1st ` v ) ) X. ( ( 2nd ` u ) ( Hom ` s ) ( 2nd ` v ) ) ) ) / h ]_ { <. ( Base ` ndx ) , b >. , <. ( Hom ` ndx ) , h >. , <. ( comp ` ndx ) , ( x e. ( b X. b ) , y e. b > ( g e. ( ( 2nd ` x ) h y ) , f e. ( h ` x ) > <. ( ( 1st ` g ) ( <. ( 1st ` ( 1st ` x ) ) , ( 1st ` ( 2nd ` x ) ) >. ( comp ` r ) ( 1st ` y ) ) ( 1st ` f ) ) , ( ( 2nd ` g ) ( <. ( 2nd ` ( 1st ` x ) ) , ( 2nd ` ( 2nd ` x ) ) >. ( comp ` s ) ( 2nd ` y ) ) ( 2nd ` f ) ) >. ) ) >. } e. _V 
5 
1 4

fnmpoi 
 Xc. Fn ( _V X. _V ) 