let g, f be Function; :: thesis: for A being set st g in sproduct f holds
g | A in sproduct (f | A)
let A be set ; :: thesis: ( g in sproduct f implies g | A in sproduct (f | A) )
A1: ( dom (g | A) = (dom g) /\ A & dom (f | A) = (dom f) /\ A ) by RELAT_1:90;
assume A2: g in sproduct f ; :: thesis: g | A in sproduct (f | A)
then A3: dom (g | A) c= dom (f | A) by A1, Th65, XBOOLE_1:26;

now

let x be set ; :: thesis: ( x in dom (g | A) implies (g | A) . x in (f | A) . x )
assume A4: x in dom (g | A) ; :: thesis: (g | A) . x in (f | A) . x
then A5: ( (g | A) . x = g . x & (f | A) . x = f . x ) by A3, FUNCT_1:70;
x in dom g by A1, A4, XBOOLE_0:def 4;
hence (g | A) . x in (f | A) . x by A2, A5, Th65; :: thesis: verum

end;

hence g | A in sproduct (f | A) by A3, Def9; :: thesis: verum