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 A3: i in I ; :: thesis: (EnsCatCoproduct A) . i = (I --> {}) . i
A4: Coprod A is V6() by A2, Th7;
thus (EnsCatCoproduct A) . i = (Coprod A) . i by A1, Def11
.= {} by A4
.= (I --> {}) . i by A3, FUNCOP_1:7 ; :: thesis: verum