let C1, C2 be non empty transitive AltCatStr ; :: thesis: ( the carrier of C1 = F₁() & ( for a, b being Object of C1 holds <^a,b^> = F₂(a,b) ) & ( for a, b, c being Object of C1 st <^a,b^> <> {} & <^b,c^> <> {} holds
for f being Morphism of a,b
for g being Morphism of b,c holds g * f = F₃(a,b,c,f,g) ) & the carrier of C2 = F₁() & ( for a, b being Object of C2 holds <^a,b^> = F₂(a,b) ) & ( for a, b, c being Object of C2 st <^a,b^> <> {} & <^b,c^> <> {} holds
for f being Morphism of a,b
for g being Morphism of b,c holds g * f = F₃(a,b,c,f,g) ) implies AltCatStr(# the carrier of C1, the Arrows of C1, the Comp of C1 #) = AltCatStr(# the carrier of C2, the Arrows of C2, the Comp of C2 #) )
assume that
A1: the carrier of C1 = F₁() and
A2: for a, b being Object of C1 holds <^a,b^> = F₂(a,b) and
A3: for a, b, c being Object of C1 st <^a,b^> <> {} & <^b,c^> <> {} holds
for f being Morphism of a,b
for g being Morphism of b,c holds g * f = F₃(a,b,c,f,g) and
A4: the carrier of C2 = F₁() and
A5: for a, b being Object of C2 holds <^a,b^> = F₂(a,b) and
A6: for a, b, c being Object of C2 st <^a,b^> <> {} & <^b,c^> <> {} holds
for f being Morphism of a,b
for g being Morphism of b,c holds g * f = F₃(a,b,c,f,g) ; :: thesis: AltCatStr(# the carrier of C1, the Arrows of C1, the Comp of C1 #) = AltCatStr(# the carrier of C2, the Arrows of C2, the Comp of C2 #)

A7: now :: thesis: for i being object st i in [:F₁(),F₁():] holds
the Arrows of C1 . i = the Arrows of C2 . i

let i be object ; :: thesis: ( i in [:F₁(),F₁():] implies the Arrows of C1 . i = the Arrows of C2 . i )
assume i in [:F₁(),F₁():] ; :: thesis: the Arrows of C1 . i = the Arrows of C2 . i
then consider a, b being object such that
A8: a in F₁() and
A9: b in F₁() and
A10: i = [a,b] by ZFMISC_1:def 2;
reconsider a1 = a, b1 = b as Object of C1 by A1, A8, A9;
reconsider a2 = a, b2 = b as Object of C2 by A4, A8, A9;
thus the Arrows of C1 . i = <^a1,b1^> by A10
.= F₂(a1,b1) by A2
.= <^a2,b2^> by A5
.= the Arrows of C2 . i by A10 ; :: thesis: verum

end;

then A11: the Arrows of C1 = the Arrows of C2 by A1, A4, PBOOLE:3;

now :: thesis: for i being object st i in [:F₁(),F₁(),F₁():] holds
the Comp of C1 . i = the Comp of C2 . i

let i be object ; :: thesis: ( i in [:F₁(),F₁(),F₁():] implies the Comp of C1 . i = the Comp of C2 . i )
assume i in [:F₁(),F₁(),F₁():] ; :: thesis: the Comp of C1 . i = the Comp of C2 . i
then consider a, b, c being object such that
A12: a in F₁() and
A13: b in F₁() and
A14: c in F₁() and
A15: i = [a,b,c] by MCART_1:68;
reconsider a1 = a, b1 = b, c1 = c as Object of C1 by A1, A12, A13, A14;
reconsider a2 = a, b2 = b, c2 = c as Object of C2 by A4, A12, A13, A14;
A16: the Comp of C1 . i = the Comp of C1 . (a1,b1,c1) by A15, MULTOP_1:def 1;
A17: the Comp of C2 . i = the Comp of C2 . (a2,b2,c2) by A15, MULTOP_1:def 1;

A18: now :: thesis: ( [:<^b1,c1^>,<^a1,b1^>:] <> {} implies <^a1,c1^> <> {} )

assume A19: [:<^b1,c1^>,<^a1,b1^>:] <> {} ; :: thesis: <^a1,c1^> <> {}
then A20: <^b1,c1^> <> {} by ZFMISC_1:90;
<^a1,b1^> <> {} by A19, ZFMISC_1:90;
hence <^a1,c1^> <> {} by A20, ALTCAT_1:def 2; :: thesis: verum

end;

then A21: dom ( the Comp of C1 . (a1,b1,c1)) = [:<^b1,c1^>,<^a1,b1^>:] by FUNCT_2:def 1;
A22: dom ( the Comp of C2 . (a2,b2,c2)) = [:<^b1,c1^>,<^a1,b1^>:] by A11, A18, FUNCT_2:def 1;

now :: thesis: for j being object st j in [:<^b1,c1^>,<^a1,b1^>:] holds
( the Comp of C1 . (a1,b1,c1)) . j = ( the Comp of C2 . (a2,b2,c2)) . j

let j be object ; :: thesis: ( j in [:<^b1,c1^>,<^a1,b1^>:] implies ( the Comp of C1 . (a1,b1,c1)) . j = ( the Comp of C2 . (a2,b2,c2)) . j )
assume j in [:<^b1,c1^>,<^a1,b1^>:] ; :: thesis: ( the Comp of C1 . (a1,b1,c1)) . j = ( the Comp of C2 . (a2,b2,c2)) . j
then consider j1, j2 being object such that
A23: j1 in <^b1,c1^> and
A24: j2 in <^a1,b1^> and
A25: j = [j1,j2] by ZFMISC_1:def 2;
reconsider j1 = j1 as Morphism of b1,c1 by A23;
reconsider j2 = j2 as Morphism of a1,b1 by A24;
reconsider f1 = j1 as Morphism of b2,c2 by A1, A4, A7, PBOOLE:3;
reconsider f2 = j2 as Morphism of a2,b2 by A1, A4, A7, PBOOLE:3;
thus ( the Comp of C1 . (a1,b1,c1)) . j = ( the Comp of C1 . (a1,b1,c1)) . (j1,j2) by A25
.= j1 * j2 by A23, A24, ALTCAT_1:def 8
.= F₃(a1,b1,c1,j2,j1) by A3, A23, A24
.= f1 * f2 by A6, A11, A23, A24
.= ( the Comp of C2 . (a2,b2,c2)) . (f1,f2) by A11, A23, A24, ALTCAT_1:def 8
.= ( the Comp of C2 . (a2,b2,c2)) . j by A25 ; :: thesis: verum

end;

hence the Comp of C1 . i = the Comp of C2 . i by A16, A17, A21, A22; :: thesis: verum

end;

hence AltCatStr(# the carrier of C1, the Arrows of C1, the Comp of C1 #) = AltCatStr(# the carrier of C2, the Arrows of C2, the Comp of C2 #) by A1, A4, A11, PBOOLE:3; :: thesis: verum