let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (uncurry f) or x in Y )
assume x in rng (uncurry f) ; :: thesis: x in Y
then consider y being object such that
A3: y in dom (uncurry f) and
A4: x = (uncurry f) . y by FUNCT_1:def 3;
consider z being object , g being Function, t being object such that
A5: y = [z,t] and
A6: ( z in dom f & g = f . z ) and
A7: t in dom g by A3, Def2;
g in rng f by A6, FUNCT_1:def 3;
then A8: ex g1 being Function st
( g = g1 & dom g1 c= X & rng g1 c= Y ) by A1, PARTFUN1:def 3;
( (uncurry f) . (z,t) = g . t & g . t in rng g ) by A6, A7, Th31, FUNCT_1:def 3;
hence x in Y by A4, A5, A8; :: thesis: verum