let f, g 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 by RELAT_1:61;
A2: dom (f | A) = (dom f) /\ A by RELAT_1:61;
assume A3: g in sproduct f ; :: thesis: g | A in sproduct (f | A)
then A4: dom (g | A) c= dom (f | A) by A1, A2, Th49, XBOOLE_1:26;
now :: thesis: for x being object st x in dom (g | A) holds
(g | A) . x in (f | A) . x
let x be object ; :: thesis: ( x in dom (g | A) implies (g | A) . x in (f | A) . x )
assume A5: x in dom (g | A) ; :: thesis: (g | A) . x in (f | A) . x
then A6: (g | A) . x = g . x by FUNCT_1:47;
A7: (f | A) . x = f . x by A4, A5, FUNCT_1:47;
x in dom g by A1, A5, XBOOLE_0:def 4;
hence (g | A) . x in (f | A) . x by A3, A6, A7, Th49; :: thesis: verum
end;
hence g | A in sproduct (f | A) by A4, Def9; :: thesis: verum