let I be set ; for A being ObjectsFamily of I,(EnsCat {{}})
for o being Object of (EnsCat {{}}) holds I --> {} is MorphismsFamily of A,o
let A be ObjectsFamily of I,(EnsCat {{}}); for o being Object of (EnsCat {{}}) holds I --> {} is MorphismsFamily of A,o
let o be Object of (EnsCat {{}}); I --> {} is MorphismsFamily of A,o
let i be object ; ALTCAT_6:def 1 ( i in I implies ex o1 being Object of (EnsCat {{}}) st
( o1 = A . i & (I --> {}) . i is Morphism of o1,o ) )
assume A1:
i in I
; ex o1 being Object of (EnsCat {{}}) st
( o1 = A . i & (I --> {}) . i is Morphism of o1,o )
reconsider I = I as non empty set by A1;
reconsider j = i as Element of I by A1;
reconsider A1 = A as ObjectsFamily of I,(EnsCat {{}}) ;
reconsider o1 = A1 . j as Object of (EnsCat {{}}) ;
take
o1
; ( o1 = A . i & (I --> {}) . i is Morphism of o1,o )
thus
o1 = A . i
; (I --> {}) . i is Morphism of o1,o
thus
(I --> {}) . i is Morphism of o1,o
by Lm3; verum