let f be Function; :: thesis: product f c= Funcs ((dom f),(Union f))
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in product f or x in Funcs ((dom f),(Union f)) )
assume x in product f ; :: thesis: x in Funcs ((dom f),(Union f))
then consider g being Function such that
A1: x = g and
A2: dom g = dom f and
A3: for x being set st x in dom f holds
g . x in f . x by CARD_3:def 5;
rng g c= Union f

proof

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

end;

hence x in Funcs ((dom f),(Union f)) by A1, A2, FUNCT_2:def 2; :: thesis: verum