let f, g be Function; :: thesis: for A being set st g in product f holds
g | A in sproduct f
let A be set ; :: thesis: ( g in product f implies g | A in sproduct f )
A1: product f c= sproduct f by Th51;
assume g in product f ; :: thesis: g | A in sproduct f
hence g | A in sproduct f by A1, Th64, RELAT_1:59; :: thesis: verum