let C1, C2 be semi-functional para-functional category; :: thesis: ( the carrier of C1 = F₁() & ( for a, b being Element of F₁()
for f being Function holds
( f in the Arrows of C1 . (a,b) iff ( f in Funcs (F₂(a),F₂(b)) & P₁[a,b,f] ) ) ) & the carrier of C2 = F₁() & ( for a, b being Element of F₁()
for f being Function holds
( f in the Arrows of C2 . (a,b) iff ( f in Funcs (F₂(a),F₂(b)) & P₁[a,b,f] ) ) ) 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 Element of F₁()
for f being Function holds
( f in the Arrows of C1 . (a,b) iff ( f in Funcs (F₂(a),F₂(b)) & P₁[a,b,f] ) ) and
A3: the carrier of C2 = F₁() and
A4: for a, b being Element of F₁()
for f being Function holds
( f in the Arrows of C2 . (a,b) iff ( f in Funcs (F₂(a),F₂(b)) & P₁[a,b,f] ) ) ; :: 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 #)
deffunc H₁( set , set ) -> set = the Arrows of C1 . ($1,$2);
A5: for C1, C2 being semi-functional para-functional category st the carrier of C1 = F₁() & ( for a, b being Object of C1 holds <^a,b^> = H₁(a,b) ) & the carrier of C2 = F₁() & ( for a, b being Object of C2 holds <^a,b^> = H₁(a,b) ) 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 19();
A6: for a, b being Object of C1 holds <^a,b^> = H₁(a,b) ;

now :: thesis: for a, b being Object of C2 holds <^a,b^> = H₁(a,b)

let a, b be Object of C2; :: thesis: <^a,b^> = H₁(a,b)
reconsider x = a, y = b as Element of F₁() by A3;
reconsider a9 = x, b9 = y as Object of C1 by A1;
thus <^a,b^> = H₁(a,b) :: thesis: verum

proof

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: H₁(a,b) c= <^a,b^>

let z be object ; :: thesis: ( z in <^a,b^> implies z in H₁(a,b) )
assume A7: z in <^a,b^> ; :: thesis: z in H₁(a,b)
then A8: z in Funcs (F₂(x),F₂(y)) by A4;
P₁[x,y,z] by A4, A7;
hence z in H₁(a,b) by A2, A8; :: thesis: verum

end;

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in H₁(a,b) or z in <^a,b^> )
assume A9: z in H₁(a,b) ; :: thesis: z in <^a,b^>
then A10: z is Morphism of a9,b9 ;
then A11: z in Funcs (F₂(x),F₂(y)) by A2, A9;
P₁[x,y,z] by A2, A9, A10;
hence z in <^a,b^> by A4, A11; :: thesis: verum

end;

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, A3, A5, A6; :: thesis: verum