let f be Function; :: thesis: product f c= sproduct f
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in product f or x in sproduct f )
assume x in product f ; :: thesis: x in sproduct f
then ex g being Function st
( x = g & dom g = dom f & ( for x being object st x in dom f holds
g . x in f . x ) ) by Def5;
hence x in sproduct f by Def9; :: thesis: verum