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: