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 :: thesis: for a being Element of F₁() holds C1 -carrier_of a = C2 -carrier_of a

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 :: thesis: for x being object holds
( x in the_carrier_of a1 iff x in the_carrier_of a2 )

let x be object ; :: 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 :: thesis: 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] ) )

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] ) )
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: 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