scheme :: YELLOW18:sch 21
ConcreteCategoryUniq3{ F1() -> non empty set , F2( object ) -> set , P1[ object , object ], P2[ object , object , object ] } :
for C1, C2 being semi-functional para-functional category st the carrier of C1 = F1() & ( for a being Object of C1
for x being set holds
( x in the_carrier_of a iff ( x in F2(a) & P1[a,x] ) ) ) & ( for a, b being Element of F1()
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)) & P2[a,b,f] ) ) ) & the carrier of C2 = F1() & ( for a being Object of C2
for x being set holds
( x in the_carrier_of a iff ( x in F2(a) & P1[a,x] ) ) ) & ( for a, b being Element of F1()
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)) & P2[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 #)