let C1, C2 be semi-functional para-functional category; :: thesis: ( the carrier of C1 = F₁() & ( 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] ) ) ) & ( 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] ) ) ) & the carrier of C2 = F₁() & ( 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] ) ) ) & ( 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] ) ) ) 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 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: 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 = 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();

A8: now

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

now

let x be set ; :: thesis: ( x in the_carrier_of a1 iff x in the_carrier_of a2 )
( 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: verum

end;

hence C1 -carrier_of a = C2 -carrier_of a by TARSKI:2; :: thesis: verum

end;

now

let a, b be Element of F₁(); :: thesis: 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] ) )
let f be Function; :: thesis: ( f in the Arrows of C2 . a,b iff ( f in Funcs H₁(a),H₁(b) & P₂[a,b,f] ) )
( H₁(a) = C2 -carrier_of a & 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; :: thesis: verum

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: verum