let C1, C2 be semi-functional para-functional category; :: thesis:
assume that
A1: the carrier of C1 = F₁() and
A2: for a being object of C1
for x being set holds
( x in the_carrier_of a iff ( x in F₂(a) & P₁[a,x] ) ) and
A3: for a, b being Element of F₁()
for f being Function holds
( f in the Arrows of C1 . a,b iff ( f in Funcs (C1 -carrier_of a),(C1 -carrier_of b) & P₂[a,b,f] ) ) and
A4: the carrier of C2 = F₁() and
A5: for a being object of C2
for x being set holds
( x in the_carrier_of a iff ( x in F₂(a) & P₁[a,x] ) ) and
A6: for a, b being Element of F₁()
for f being Function holds
( f in the Arrows of C2 . a,b iff ( f in Funcs (C2 -carrier_of a),(C2 -carrier_of b) & P₂[a,b,f] ) ) ; :: thesis:
deffunc H₁( set ) -> set = C1 -carrier_of $1;
A7: for C1, C2 being semi-functional para-functional category st 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 H₁(a),H₁(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 H₁(a),H₁(b) & P₂[a,b,f] ) ) ) 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 20();

let a be Element of F₁(); :: thesis:
reconsider a1 = a as object of C1 by A1;
reconsider a2 = a as object of C2 by A4;

let x be set ; :: thesis:
( x in the_carrier_of a1 iff ( x in F₂(a) & P₁[a,x] ) ) by A2;
hence ( x in the_carrier_of a1 iff x in the_carrier_of a2 ) by A5; :: thesis:

end;

end;

let a, b be Element of F₁(); :: thesis:
let f be Function; :: thesis:
A9: H₁(a) = C2 -carrier_of a by A8;
H₁(b) = C2 -carrier_of b by A8;
hence ( f in the Arrows of C2 . a,b iff ( f in Funcs H₁(a),H₁(b) & P₂[a,b,f] ) ) by A6, A9; :: thesis:

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, A4, A7; :: thesis: