deffunc H1( set , set , set , set , set ) -> set = $4 (#) $5;
A1:
for C1, C2 being non empty transitive AltCatStr st the carrier of C1 = F1() & ( for a, b being Object of C1 holds <^a,b^> = F2(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 = H1(a,b,c,f,g) ) & the carrier of C2 = F1() & ( for a, b being Object of C2 holds <^a,b^> = F2(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 = H1(a,b,c,f,g) ) holds
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 #)
from YELLOW18:sch 5();
let C1, C2 be semi-functional para-functional category; ( the carrier of C1 = F1() & ( for a, b being Object of C1 holds <^a,b^> = F2(a,b) ) & the carrier of C2 = F1() & ( for a, b being Object of C2 holds <^a,b^> = F2(a,b) ) 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 #) )
A2:
for C1 being semi-functional para-functional category
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 (#) g
by Th36;
then 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 (#) g
;
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 (#) g
by A2;
hence
( the carrier of C1 = F1() & ( for a, b being Object of C1 holds <^a,b^> = F2(a,b) ) & the carrier of C2 = F1() & ( for a, b being Object of C2 holds <^a,b^> = F2(a,b) ) 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 #) )
by A1, A3; verum