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 :: thesis: for i, j, k being object st i in F₁() & j in F₁() & k in F₁() holds
the Comp of C1 . (i,j,k) = the Comp of C2 . (i,j,k)

let i, j, k be object ; :: 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 :: thesis: for i, j being Element of F₁() holds the Arrows of C1 . (i,j) = the Arrows of C2 . (i,j)

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:7;
hence C1 = C2 by A1, A3, A5, ALTCAT_1:8; :: thesis: verum