let f, g be Function; :: thesis: ( f c= g implies sproduct f c= sproduct g )
assume A1: f c= g ; :: thesis: sproduct f c= sproduct g
then A2: dom f c= dom g by GRFUNC_1:8;
let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in sproduct f or y in sproduct g )
assume y in sproduct f ; :: thesis: y in sproduct g
then consider h being Function such that
A3: ( y = h & dom h c= dom f ) and
A4: for x being set st x in dom h holds
h . x in f . x by Def9;
A5: dom h c= dom g by A2, A3, XBOOLE_1:1;

now

let x be set ; :: thesis: ( x in dom h implies h . x in g . x )
assume A6: x in dom h ; :: thesis: h . x in g . x
then f . x = g . x by A1, A3, GRFUNC_1:8;
hence h . x in g . x by A4, A6; :: thesis: verum

end;

hence y in sproduct g by A3, A5, Def9; :: thesis: verum