let I be set ; for A being ObjectsFamily of I,(EnsCat {{}})
for o being Object of (EnsCat {{}})
for P being MorphismsFamily of A,o st P = I --> {} holds
( P is feasible & P is coprojection-morphisms )
let A be ObjectsFamily of I,(EnsCat {{}}); for o being Object of (EnsCat {{}})
for P being MorphismsFamily of A,o st P = I --> {} holds
( P is feasible & P is coprojection-morphisms )
let o be Object of (EnsCat {{}}); for P being MorphismsFamily of A,o st P = I --> {} holds
( P is feasible & P is coprojection-morphisms )
let P be MorphismsFamily of A,o; ( P = I --> {} implies ( P is feasible & P is coprojection-morphisms ) )
assume A1:
P = I --> {}
; ( P is feasible & P is coprojection-morphisms )
thus
P is feasible
P is coprojection-morphisms
let Y be Object of (EnsCat {{}}); ALTCAT_6:def 5 for F being MorphismsFamily of A,Y st F is feasible holds
ex f being Morphism of o,Y st
( f in <^o,Y^> & ( 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 ) ) & ( 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 ) )
let F be MorphismsFamily of A,Y; ( F is feasible implies ex f being Morphism of o,Y st
( f in <^o,Y^> & ( 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 ) ) & ( 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 ) ) )
assume
F is feasible
; ex f being Morphism of o,Y st
( f in <^o,Y^> & ( 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 ) ) & ( 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 ) )
reconsider f = {} as Morphism of o,Y by Lm3;
take
f
; ( f in <^o,Y^> & ( 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 ) ) & ( 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 ) )
thus
f in <^o,Y^>
by Lm3; ( ( 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 ) ) & ( 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 ) )
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 )
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
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; verum