let x be set ; :: thesis: for h, f being Function st x c= h & h in sproduct f holds
x in sproduct f
let h, f be Function; :: 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, Th65;
then A4: dom g c= dom f by A3, XBOOLE_1:1;

now

let x be set ; :: 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, Th65;
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