let x be object ; :: according to VALUED_2:def 3 :: thesis: ( x in PFuncs (X,Y) implies x is ext-real-valued Function )

assume x in PFuncs (X,Y) ; :: thesis: x is ext-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 3;

reconsider f = f as PartFunc of X,Y by A2, RELSET_1:4;

f is set ;

hence x is ext-real-valued Function by A1; :: thesis: verum

assume x in PFuncs (X,Y) ; :: thesis: x is ext-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 3;

reconsider f = f as PartFunc of X,Y by A2, RELSET_1:4;

f is set ;

hence x is ext-real-valued Function by A1; :: thesis: verum