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

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