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₁() & ( 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
A2: ( 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) ) ) ) ) ; :: thesis: C1 = C2

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 A1
.= the Arrows of C2 . i,j by A2 ; :: thesis: verum

end;

then A3: the Arrows of C1 = the Arrows of C2 by A1, A2, ALTCAT_1:9;

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 A4: ( 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 A1
.= the Comp of C2 . i,j,k by A2, A4 ;
:: thesis: verum

end;

hence C1 = C2 by A1, A2, A3, ALTCAT_1:10; :: thesis: verum