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

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