let f, g be Function; :: thesis: ( g in product f iff ( dom g = dom f & ( for x being object st x in dom f holds
g . x in f . x ) ) )
thus ( g in product f implies ( dom g = dom f & ( for x being object st x in dom f holds
g . x in f . x ) ) ) :: thesis: ( dom g = dom f & ( for x being object st x in dom f holds
g . x in f . x ) implies g in product f )

proof

assume g in product f ; :: thesis: ( dom g = dom f & ( for x being object st x in dom f holds
g . x in f . x ) )
then ex h being Function st
( g = h & dom h = dom f & ( for x being object st x in dom f holds
h . x in f . x ) ) by Def5;
hence ( dom g = dom f & ( for x being object st x in dom f holds
g . x in f . x ) ) ; :: thesis: verum

end;

thus ( dom g = dom f & ( for x being object st x in dom f holds
g . x in f . x ) implies g in product f ) by Def5; :: thesis: verum