let I be set ; :: thesis: 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 {{}}); :: thesis: for o being Object of (EnsCat {{}}) holds I --> {} is MorphismsFamily of A,o
let o be Object of (EnsCat {{}}); :: thesis: I --> {} is MorphismsFamily of A,o
let i be object ; :: according to ALTCAT_6:def 1 :: thesis: ( 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 ; :: thesis: 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 ; :: thesis: ( o1 = A . i & (I --> {}) . i is Morphism of o1,o )
thus o1 = A . i ; :: thesis: (I --> {}) . i is Morphism of o1,o
thus (I --> {}) . i is Morphism of o1,o by Lm3; :: thesis: verum