let f be Function; :: thesis: for X being set
for i being object st i in dom f & X c= f . i holds
product (f +* (i,X)) c= product f
let X be set ; :: thesis: for i being object st i in dom f & X c= f . i holds
product (f +* (i,X)) c= product f
let i be object ; :: thesis: ( i in dom f & X c= f . i implies product (f +* (i,X)) c= product f )
I: i is set by TARSKI:1;
assume ( i in dom f & X c= f . i ) ; :: thesis: product (f +* (i,X)) c= product f
then product (f +* (i,X)) c= product (f +* (i,(f . i))) by Th38;
hence product (f +* (i,X)) c= product f by I, FUNCT_7:35; :: thesis: verum