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 A,o; :: thesis:
assume A1: P = I --> {} ; :: thesis:
thus P is feasible :: thesis:

proof

let i be set ; :: according to ALTCAT_6:def 3 :: 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, FUNCOP_1:7;
then P . i in <^(A . i),o^> 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_6:def 5 :: thesis:
let F be MorphismsFamily of A,Y; :: thesis:
assume F is feasible ; :: thesis:
reconsider f = {} as Morphism of o,Y by Lm3;
take f ; :: thesis:
thus f in <^o,Y^> by Lm3; :: thesis:
thus for i being set st i in I holds
ex si being Object of (EnsCat {{}}) ex Pi being Morphism of si,o st
( si = A . i & Pi = P . i & F . i = f * Pi ) :: 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 A1,Y ;
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, A3, FUNCOP_1:7; :: thesis:
( F1 . j is Morphism of o,Y & f * M is Morphism of o,Y ) by Lm5;
hence F . i = f * M by Lm6; :: thesis:

end;

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