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