let C1, C2 be strict AltCatStr ; :: thesis: ( the carrier of C1 = F1() & ( for i, j being Element of F1() holds
( the Arrows of C1 . (i,j) = F2(i,j) & ( for i, j, k being Element of F1() holds the Comp of C1 . (i,j,k) = FuncComp (F2(i,j),F2(j,k)) ) ) ) & the carrier of C2 = F1() & ( for i, j being Element of F1() holds
( the Arrows of C2 . (i,j) = F2(i,j) & ( for i, j, k being Element of F1() holds the Comp of C2 . (i,j,k) = FuncComp (F2(i,j),F2(j,k)) ) ) ) implies C1 = C2 )

assume that
A1: the carrier of C1 = F1() and
A2: for i, j being Element of F1() holds
( the Arrows of C1 . (i,j) = F2(i,j) & ( for i, j, k being Element of F1() holds the Comp of C1 . (i,j,k) = FuncComp (F2(i,j),F2(j,k)) ) ) and
A3: the carrier of C2 = F1() and
A4: for i, j being Element of F1() holds
( the Arrows of C2 . (i,j) = F2(i,j) & ( for i, j, k being Element of F1() holds the Comp of C2 . (i,j,k) = FuncComp (F2(i,j),F2(j,k)) ) ) ; :: thesis: C1 = C2
A5: now :: thesis: for i, j, k being object st i in F1() & j in F1() & k in F1() holds
the Comp of C1 . (i,j,k) = the Comp of C2 . (i,j,k)
let i, j, k be object ; :: thesis: ( i in F1() & j in F1() & k in F1() implies the Comp of C1 . (i,j,k) = the Comp of C2 . (i,j,k) )
assume A6: ( i in F1() & j in F1() & k in F1() ) ; :: thesis: the Comp of C1 . (i,j,k) = the Comp of C2 . (i,j,k)
hence the Comp of C1 . (i,j,k) = FuncComp (F2(i,j),F2(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 F1() holds the Arrows of C1 . (i,j) = the Arrows of C2 . (i,j)
let i, j be Element of F1(); :: thesis: the Arrows of C1 . (i,j) = the Arrows of C2 . (i,j)
thus the Arrows of C1 . (i,j) = F2(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 ;
hence C1 = C2 by ; :: thesis: verum