let a be Real; :: thesis:
let A be non empty set ; :: thesis:
let f, h be Element of PFuncs (A,REAL); :: thesis:

hereby :: thesis:

assume A1: h = (multrealpfunc A) . (a,f) ; :: thesis:
then dom h = dom (a (#) f) by Def4;
hence dom h = dom f by VALUED_1:def 5; :: thesis:
let x be Element of A; :: thesis:
assume x in dom f ; :: thesis:
then x in dom (a (#) f) by VALUED_1:def 5;
then (a (#) f) . x = a * (f . x) by VALUED_1:def 5;
hence h . x = a * (f . x) by A1, Def4; :: thesis:

end;

hereby :: thesis:

reconsider aa = a as Element of REAL by XREAL_0:def 1;
reconsider k = (multrealpfunc A) . (aa,f) as Element of PFuncs (A,REAL) ;
assume that
A2: dom f = dom h and
A3: for x being Element of A st x in dom f holds
h . x = a * (f . x) ; :: thesis:

A4: now :: thesis:

let x be Element of A; :: thesis:
assume A5: x in dom f ; :: thesis:
then x in dom (a (#) f) by VALUED_1:def 5;
then (a (#) f) . x = a * (f . x) by VALUED_1:def 5;
then (a (#) f) . x = h . x by A3, A5;
hence k . x = h . x by Def4; :: thesis:

end;

k = a (#) f by Def4;
then dom k = dom f by VALUED_1:def 5;
hence h = (multrealpfunc A) . (a,f) by A2, A4, PARTFUN1:5; :: thesis:

end;