for C1, C2 being semi-functional para-functional category st the carrier of C1 = the carrier of C & ( for a being Object of C1
for x being set holds
( x in the_carrier_of a iff ( x in H₁(a) & S₁[a,x] ) ) ) & ( for a, b being Element of C
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)) & S₂[a,b,f] ) ) ) & the carrier of C2 = the carrier of C & ( for a being Object of C2
for x being set holds
( x in the_carrier_of a iff ( x in H₁(a) & S₁[a,x] ) ) ) & ( for a, b being Element of C
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)) & S₂[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 21();
hence for b₁, b₂ being strict concrete category st the carrier of b₁ = the carrier of C & ( for a being Object of b₁
for x being set holds
( x in the_carrier_of a iff ( x in Union (disjoin the Arrows of C) & a = x `22 ) ) ) & ( for a, b being Element of C
for f being Function holds
( f in the Arrows of b₁ . (a,b) iff ( f in Funcs ((b₁ -carrier_of a),(b₁ -carrier_of b)) & ex fa, fb being Object of C ex g being Morphism of fa,fb st
( fa = a & fb = b & <^fa,fb^> <> {} & ( for o being Object of C st <^o,fa^> <> {} holds
for h being Morphism of o,fa holds f . [h,[o,fa]] = [(g * h),[o,fb]] ) ) ) ) ) & the carrier of b₂ = the carrier of C & ( for a being Object of b₂
for x being set holds
( x in the_carrier_of a iff ( x in Union (disjoin the Arrows of C) & a = x `22 ) ) ) & ( for a, b being Element of C
for f being Function holds
( f in the Arrows of b₂ . (a,b) iff ( f in Funcs ((b₂ -carrier_of a),(b₂ -carrier_of b)) & ex fa, fb being Object of C ex g being Morphism of fa,fb st
( fa = a & fb = b & <^fa,fb^> <> {} & ( for o being Object of C st <^o,fa^> <> {} holds
for h being Morphism of o,fa holds f . [h,[o,fa]] = [(g * h),[o,fb]] ) ) ) ) ) holds
b₁ = b₂ ; :: thesis: