let C1, C2 be strict AltCatStr ; :: thesis: ( the carrier of C1 = F₁() & ( for i, j being Element of F₁() holds
( the Arrows of C1 . i,j = F₂(i,j) & ( for i, j, k being Element of F₁() holds the Comp of C1 . i,j,k = FuncComp F₂(i,j),F₂(j,k) ) ) ) & the carrier of C2 = F₁() & ( for i, j being Element of F₁() holds
( the Arrows of C2 . i,j = F₂(i,j) & ( for i, j, k being Element of F₁() holds the Comp of C2 . i,j,k = FuncComp F₂(i,j),F₂(j,k) ) ) ) implies C1 = C2 )
assume that
A1: the carrier of C1 = F₁() and
A2: for i, j being Element of F₁() holds
( the Arrows of C1 . i,j = F₂(i,j) & ( for i, j, k being Element of F₁() holds the Comp of C1 . i,j,k = FuncComp F₂(i,j),F₂(j,k) ) ) and
A3: the carrier of C2 = F₁() and
A4: for i, j being Element of F₁() holds
( the Arrows of C2 . i,j = F₂(i,j) & ( for i, j, k being Element of F₁() holds the Comp of C2 . i,j,k = FuncComp F₂(i,j),F₂(j,k) ) ) ; :: thesis: C1 = C2

A5: now

let i, j, k be set ; :: thesis: ( i in F₁() & j in F₁() & k in F₁() implies the Comp of C1 . i,j,k = the Comp of C2 . i,j,k )
assume A6: ( i in F₁() & j in F₁() & k in F₁() ) ; :: thesis: the Comp of C1 . i,j,k = the Comp of C2 . i,j,k
hence the Comp of C1 . i,j,k = FuncComp F₂(i,j),F₂(j,k) by A2
.= the Comp of C2 . i,j,k by A4, A6 ;
:: thesis: verum

end;

now

let i, j be Element of F₁(); :: thesis: the Arrows of C1 . i,j = the Arrows of C2 . i,j
thus the Arrows of C1 . i,j = F₂(i,j) by A2
.= the Arrows of C2 . i,j by A4 ; :: thesis: verum

end;

then the Arrows of C1 = the Arrows of C2 by A1, A3, ALTCAT_1:9;
hence C1 = C2 by A1, A3, A5, ALTCAT_1:10; :: thesis: verum