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:2;
let y be object ; :: 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 and
A4: dom h c= dom f and
A5: for x being object st x in dom h holds
h . x in f . x by Def9;
A6: dom h c= dom g by A2, A4;
now :: thesis: for x being object st x in dom h holds
h . x in g . x
let x be object ; :: thesis: ( x in dom h implies h . x in g . x )
assume A7: x in dom h ; :: thesis: h . x in g . x
then f . x = g . x by A1, A4, GRFUNC_1:2;
hence h . x in g . x by A5, A7; :: thesis: verum
end;
hence y in sproduct g by A3, A6, Def9; :: thesis: verum