let I be set ; :: thesis:
let A be ObjectsFamily of I,(EnsCat {{}}); :: thesis:
let o be Object of (EnsCat {{}}); :: thesis:
let P be MorphismsFamily of o,A; :: thesis:
assume A1: P = I --> {} ; :: thesis:
thus P is feasible :: thesis:

proof

let i be set ; :: according to ALTCAT_5:def 4 :: thesis:
assume A2: i in I ; :: thesis:
then reconsider I = I as non empty set ;
reconsider i = i as Element of I by A2;
reconsider A = A as ObjectsFamily of I,(EnsCat {{}}) ;
P . i = {} by A1;
then P . i in <^o,(A . i)^> by Lm3;
hence ex o being Object of (EnsCat {{}}) st
( o = A . i & P . i in <^o,o^> ) ; :: thesis:

end;

let Y be Object of (EnsCat {{}}); :: according to ALTCAT_5:def 6 :: thesis:
let F be MorphismsFamily of Y,A; :: thesis:
assume F is feasible ; :: thesis:
reconsider f = {} as Morphism of Y,o by Lm3;
take f ; :: thesis:
thus f in <^Y,o^> by Lm3; :: thesis:
thus for i being set st i in I holds
ex si being Object of (EnsCat {{}}) ex Pi being Morphism of o,si st
( si = A . i & Pi = P . i & F . i = Pi * f ) :: thesis:

proof

let i be set ; :: thesis:
assume A3: i in I ; :: thesis:
then reconsider I = I as non empty set ;
reconsider j = i as Element of I by A3;
reconsider M = {} as Morphism of o,o by Lm3;
reconsider A1 = A as ObjectsFamily of I,(EnsCat {{}}) ;
reconsider F1 = F as MorphismsFamily of Y,A1 ;
take o ; :: thesis:
take M ; :: thesis:
A1 . j = {} by Lm1, TARSKI:def 1;
hence o = A . i by Lm5; :: thesis:
thus M = P . i by A1; :: thesis:
( F1 . j is Morphism of Y,o & M * f is Morphism of Y,o ) by Lm5;
hence F . i = M * f by Lm6; :: thesis:

end;

thus for f1 being Morphism of Y,o st ( for i being set st i in I holds
ex si being Object of (EnsCat {{}}) ex Pi being Morphism of o,si st
( si = A . i & Pi = P . i & F . i = Pi * f1 ) ) holds
f = f1 by Lm4; :: thesis: