let f, g be Function; :: thesis: ( g in sproduct f implies ( dom g c= dom f & ( for x being object st x in dom g holds
g . x in f . x ) ) )
assume g in sproduct f ; :: thesis: ( dom g c= dom f & ( for x being object st x in dom g holds
g . x in f . x ) )
then ex h being Function st
( g = h & dom h c= dom f & ( for x being object st x in dom h holds
h . x in f . x ) ) by Def9;
hence ( dom g c= dom f & ( for x being object st x in dom g holds
g . x in f . x ) ) ; :: thesis: verum