let I be set ; :: thesis: for E being non empty set
for A being ObjectsFamily of I,(EnsCat E) st Union (coprod A) in E & Union (coprod A) = {} holds
EnsCatCoproduct A = I --> {}
let E be non empty set ; :: thesis: for A being ObjectsFamily of I,(EnsCat E) st Union (coprod A) in E & Union (coprod A) = {} holds
EnsCatCoproduct A = I --> {}
let A be ObjectsFamily of I,(EnsCat E); :: thesis: ( Union (coprod A) in E & Union (coprod A) = {} implies EnsCatCoproduct A = I --> {} )
assume that
A1: Union (coprod A) in E and
A2: Union (coprod A) = {} ; :: thesis: EnsCatCoproduct A = I --> {}
let i be object ; :: according to PBOOLE:def 10 :: thesis: ( not i in I or (EnsCatCoproduct A) . i = (I --> {}) . i )
assume i in I ; :: thesis: (EnsCatCoproduct A) . i = (I --> {}) . i
A4: Coprod A is empty-yielding by A2, Th7;
thus (EnsCatCoproduct A) . i = (Coprod A) . i by A1, Def11
.= {} by A4
.= (I --> {}) . i ; :: thesis: verum