let f be non-empty Function; :: thesis: for X being set
for i being object st i in dom f & product (f +* (i,X)) c= product f holds
X c= f . i
let X be set ; :: thesis: for i being object st i in dom f & product (f +* (i,X)) c= product f holds
X c= f . i
let i be object ; :: thesis: ( i in dom f & product (f +* (i,X)) c= product f implies X c= f . i )
assume A1: ( i in dom f & product (f +* (i,X)) c= product f ) ; :: thesis: X c= f . i
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in f . i )
assume A2: x in X ; :: thesis: x in f . i
set g = the Element of product f;
a3: the Element of product f +* (i,x) in product (f +* (i,X)) by A1, A2, Th37;
i in dom the Element of product f by A1, CARD_3:9;
then ( the Element of product f +* (i,x)) . i = x by FUNCT_7:31;
hence x in f . i by A1, a3, CARD_3:9; :: thesis: verum