let x be set ; :: thesis: for f being Function st x in sproduct f holds
x is PartFunc of (dom f),(union (rng f))
let f be Function; :: thesis: ( x in sproduct f implies x is PartFunc of (dom f),(union (rng f)) )
assume x in sproduct f ; :: thesis: x is PartFunc of (dom f),(union (rng f))
then consider g being Function such that
A1: ( x = g & dom g c= dom f & ( for x being set st x in dom g holds
g . x in f . x ) ) by Def9;
rng g c= union (rng f)

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng g or y in union (rng f) )
assume y in rng g ; :: thesis: y in union (rng f)
then consider z being set such that
A2: ( z in dom g & y = g . z ) by FUNCT_1:def 5;
A3: g . z in f . z by A1, A2;
f . z in rng f by A1, A2, FUNCT_1:def 5;
hence y in union (rng f) by A2, A3, TARSKI:def 4; :: thesis: verum

end;

hence x is PartFunc of (dom f),(union (rng f)) by A1, RELSET_1:11; :: thesis: verum