let x be object ; :: according to VALUED_2:def 28 :: thesis: ( not x in dom (RealFuncMult A) or (RealFuncMult A) . x is set )
set IT = RealFuncMult A;
assume x in dom (RealFuncMult A) ; :: thesis: (RealFuncMult A) . x is set
then (RealFuncMult A) . x in Funcs (A,REAL) by PARTFUN1:4;
then (RealFuncMult A) . x is Function of A,REAL by FUNCT_2:66;
hence (RealFuncMult A) . x is real-valued Function ; :: thesis: verum