let I be set ; :: thesis: for E being non empty set
for A being ObjectsFamily of I,(EnsCat E) st product A in E & product A = {} holds
EnsCatProduct A = I --> {}
let E be non empty set ; :: thesis: for A being ObjectsFamily of I,(EnsCat E) st product A in E & product A = {} holds
EnsCatProduct A = I --> {}
let A be ObjectsFamily of I,(EnsCat E); :: thesis: ( product A in E & product A = {} implies EnsCatProduct A = I --> {} )
assume that
A1: product A in E and
A2: product A = {} ; :: thesis: EnsCatProduct A = I --> {}

now :: thesis: for i being object st i in I holds
(EnsCatProduct A) . i = (I --> {}) . i

let i be object ; :: thesis: ( i in I implies (EnsCatProduct A) . i = (I --> {}) . i )
assume i in I ; :: thesis: (EnsCatProduct A) . i = (I --> {}) . i
hence (EnsCatProduct A) . i = proj (A,i) by A1, Def11
.= {} by A2
.= (I --> {}) . i ;
:: thesis: verum

end;

hence EnsCatProduct A = I --> {} by PBOOLE:3; :: thesis: verum