deffunc H₁( set , set , set , set , set ) -> set = $4 (#) $5;
A1: for C1, C2 being non empty transitive AltCatStr st 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 = H₁(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 = H₁(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; :: thesis: ( the carrier of C1 = F₁() & ( for a, b being object of C1 holds <^a,b^> = F₂(a,b) ) & the carrier of C2 = F₁() & ( for a, b being object of C2 holds <^a,b^> = F₂(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 #) )

now

let C1 be semi-functional para-functional category; :: thesis: 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
let a, b, c be object of C1; :: thesis: ( <^a,b^> <> {} & <^b,c^> <> {} implies for f being Morphism of a,b
for g being Morphism of b,c holds g * f = f (#) g )
assume A2: ( <^a,b^> <> {} & <^b,c^> <> {} ) ; :: thesis: for f being Morphism of a,b
for g being Morphism of b,c holds g * f = f (#) g
let f be Morphism of a,b; :: thesis: for g being Morphism of b,c holds g * f = f (#) g
let g be Morphism of b,c; :: thesis: g * f = f (#) g
thus g * f = g * f by A2, Th38
.= f (#) g by YELLOW16:1 ; :: thesis: verum

end;

then ( ( 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 ) ) ;
hence ( the carrier of C1 = F₁() & ( for a, b being object of C1 holds <^a,b^> = F₂(a,b) ) & the carrier of C2 = F₁() & ( for a, b being object of C2 holds <^a,b^> = F₂(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; :: thesis: verum