let f be Function; 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 ; 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 ; ( 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 )
; 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; verum