let f be Function; :: thesis: for X, Y being set

for i being object st i in dom f & X c= Y holds

product (f +* (i,X)) c= product (f +* (i,Y))

let X, Y be set ; :: thesis: for i being object st i in dom f & X c= Y holds

product (f +* (i,X)) c= product (f +* (i,Y))

let i be object ; :: thesis: ( i in dom f & X c= Y implies product (f +* (i,X)) c= product (f +* (i,Y)) )

assume A1: ( i in dom f & X c= Y ) ; :: thesis: product (f +* (i,X)) c= product (f +* (i,Y))

then ( f +* (i,X) = f +* (i .--> X) & f +* (i,Y) = f +* (i .--> Y) ) by FUNCT_7:def 3;

hence product (f +* (i,X)) c= product (f +* (i,Y)) by A1, Th27; :: thesis: verum

for i being object st i in dom f & X c= Y holds

product (f +* (i,X)) c= product (f +* (i,Y))

let X, Y be set ; :: thesis: for i being object st i in dom f & X c= Y holds

product (f +* (i,X)) c= product (f +* (i,Y))

let i be object ; :: thesis: ( i in dom f & X c= Y implies product (f +* (i,X)) c= product (f +* (i,Y)) )

assume A1: ( i in dom f & X c= Y ) ; :: thesis: product (f +* (i,X)) c= product (f +* (i,Y))

then ( f +* (i,X) = f +* (i .--> X) & f +* (i,Y) = f +* (i .--> Y) ) by FUNCT_7:def 3;

hence product (f +* (i,X)) c= product (f +* (i,Y)) by A1, Th27; :: thesis: verum