for C1, C2 being semi-functional para-functional category st the carrier of C1 = the carrier of C & ( for a being object of
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
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
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
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
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
for f being Function holds
( f in the Arrows of b<sub>1</sub> . a,b iff ( f in Funcs (b<sub>1</sub> -carrier_of a),(b<sub>1</sub> -carrier_of b) & ex fa, fb being object of ex g being Morphism of , st
( fa = a & fb = b & <^fa,fb^> <> {} & ( for o being object of st <^o,fa^> <> {} holds
for h being Morphism of , holds f . [h,[o,fa]] = [(g * h),[o,fb]] ) ) ) ) ) & the carrier of b<sub>2</sub> = the carrier of C & ( for a being object of
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
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 ex g being Morphism of , st
( fa = a & fb = b & <^fa,fb^> <> {} & ( for o being object of st <^o,fa^> <> {} holds
for h being Morphism of , holds f . [h,[o,fa]] = [(g * h),[o,fb]] ) ) ) ) ) holds
b₁ = b₂ ; :: thesis: verum