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 )
set k = the Element of product f;
reconsider k = the Element of product f as Function ;
take k +* g ; :: thesis: ( k +* g in product f & g c= k +* g )
thus k +* g in product f by A1, A2, Th53; :: thesis: g c= k +* g
thus g c= k +* g by FUNCT_4:25; :: thesis: verum

end;

given h being Function such that A3: h in product f and
A4: g c= h ; :: thesis: g in sproduct f
A5: dom h = dom f by A3, Th9;
A6: dom g c= dom h by A4, RELAT_1:11;

now :: thesis: for x being object st x in dom g holds
g . x in f . x

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

end;

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