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 holds <^a,b^> = F₂(a,b) ) & ( for a, b, c being object of st <^a,b^> <> {} & <^b,c^> <> {} holds
for f being Morphism of ,
for g being Morphism of , holds g * f = H₁(a,b,c,f,g) ) & the carrier of C2 = F₁() & ( for a, b being object of holds <^a,b^> = F₂(a,b) ) & ( for a, b, c being object of st <^a,b^> <> {} & <^b,c^> <> {} holds
for f being Morphism of ,
for g being Morphism of , 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 holds <^a,b^> = F₂(a,b) ) & the carrier of C2 = F₁() & ( for a, b being object of 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 #) )

A2: now

let C1 be semi-functional para-functional category; :: thesis: for a, b, c being object of st <^a,b^> <> {} & <^b,c^> <> {} holds
for f being Morphism of ,
for g being Morphism of , holds g * f = f (#) g
let a, b, c be object of ; :: thesis: ( <^a,b^> <> {} & <^b,c^> <> {} implies for f being Morphism of ,
for g being Morphism of , holds g * f = f (#) g )
assume that
A3: <^a,b^> <> {} and
A4: <^b,c^> <> {} ; :: thesis: for f being Morphism of ,
for g being Morphism of , holds g * f = f (#) g
let f be Morphism of ,; :: thesis: for g being Morphism of , holds g * f = f (#) g
let g be Morphism of ,; :: thesis: g * f = f (#) g
thus g * f = g * f by A3, A4, Th38
.= f (#) g by YELLOW16:1 ; :: thesis: verum

end;

then A5: for a, b, c being object of st <^a,b^> <> {} & <^b,c^> <> {} holds
for f being Morphism of ,
for g being Morphism of , holds g * f = f (#) g ;
for a, b, c being object of st <^a,b^> <> {} & <^b,c^> <> {} holds
for f being Morphism of ,
for g being Morphism of , holds g * f = f (#) g by A2;
hence ( the carrier of C1 = F₁() & ( for a, b being object of holds <^a,b^> = F₂(a,b) ) & the carrier of C2 = F₁() & ( for a, b being object of 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, A5; :: thesis: verum