let f, h be Function; :: thesis: for x being set st x c= h & h in sproduct f holds
x in sproduct f
let x be set ; :: thesis: ( x c= h & h in sproduct f implies x in sproduct f )
assume that
A1: x c= h and
A2: h in sproduct f ; :: thesis: x in sproduct f
reconsider g = x as Function by A1;
A3: dom g c= dom h by A1, GRFUNC_1:2;
dom h c= dom f by A2, Th49;
then A4: dom g c= dom f by A3;
now :: thesis: for x being object st x in dom g holds
g . x in f . x
let x be object ; :: thesis: ( x in dom g implies g . x in f . x )
assume A5: x in dom g ; :: thesis: g . x in f . x
then h . x in f . x by A2, A3, Th49;
hence g . x in f . x by A1, A5, GRFUNC_1:2; :: thesis: verum
end;
hence x in sproduct f by A4, Def9; :: thesis: verum