let x be object ; :: 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 and
A2: dom g c= dom f and
A3: for x being object st x in dom g holds
g . x in f . x by Def9;
rng g c= union (rng f)

proof

let y be object ; :: 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 object such that
A4: z in dom g and
A5: y = g . z by FUNCT_1:def 3;
A6: g . z in f . z by A3, A4;
f . z in rng f by A2, A4, FUNCT_1:def 3;
hence y in union (rng f) by A5, A6, TARSKI:def 4; :: thesis: verum

end;

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