let x be set ; :: according to VALUED_2:def 4 :: thesis: ( x in PFuncs X,Y implies x is real-valued Function )
assume x in PFuncs X,Y ; :: thesis: x is real-valued Function
then consider f being Function such that
A1: x = f and
A2: ( dom f c= X & rng f c= Y ) by PARTFUN1:def 5;
reconsider f = f as PartFunc of X,Y by A2, RELSET_1:11;
f is set ;
hence x is real-valued Function by A1; :: thesis: verum