let I be set ; :: thesis: for E being non empty set
for A being ObjectsFamily of I,(EnsCat E) st Union (coprod A) = {} holds
A is empty-yielding
let E be non empty set ; :: thesis: for A being ObjectsFamily of I,(EnsCat E) st Union (coprod A) = {} holds
A is empty-yielding
let A be ObjectsFamily of I,(EnsCat E); :: thesis: ( Union (coprod A) = {} implies A is empty-yielding )
assume A1: Union (coprod A) = {} ; :: thesis: A is empty-yielding
let i be object ; :: according to PBOOLE:def 12 :: thesis: ( not i in I or A . i is empty )
assume i in I ; :: thesis: A . i is empty
then consider F being Function of (A . i),(Union (coprod A)) such that
(Coprod A) . i = F and
A2: for x being object st x in A . i holds
F . x = [x,i] by Def10;
assume not A . i is empty ; :: thesis: contradiction
then consider x being object such that
A3: x in A . i by XBOOLE_0:7;
F . x = [x,i] by A2, A3;
hence contradiction by A1; :: thesis: verum