let f, g be Function; :: thesis: ( product f <> {} implies ( g in sproduct f iff ex h being Function st
( h in product f & g c= h ) ) )
assume A1: product f <> {} ; :: thesis: ( g in sproduct f iff ex h being Function st
( h in product f & g c= h ) )
thus ( g in sproduct f implies ex h being Function st
( h in product f & g c= h ) ) :: thesis: ( ex h being Function st
( h in product f & g c= h ) implies g in sproduct f )

proof

assume A2: g in sproduct f ; :: thesis: ex h being Function st
( h in product f & g c= h )
consider k being Element of product f;
reconsider k = k as Function ;
take k +* g ; :: thesis: ( k +* g in product f & g c= k +* g )
thus k +* g in product f by A1, A2, Th69; :: thesis: g c= k +* g
thus g c= k +* g by FUNCT_4:26; :: thesis: verum

end;

given h being Function such that A3: ( h in product f & g c= h ) ; :: thesis: g in sproduct f
A4: ( dom h = dom f & ( for x being set st x in dom f holds
h . x in f . x ) ) by A3, Th18;
A5: dom g c= dom h by A3, RELAT_1:25;

now

let x be set ; :: thesis: ( x in dom g implies g . x in f . x )
assume A6: x in dom g ; :: thesis: g . x in f . x
then g . x = h . x by A3, GRFUNC_1:8;
hence g . x in f . x by A4, A5, A6; :: thesis: verum

end;

hence g in sproduct f by A4, A5, Def9; :: thesis: verum