let a be Real; :: thesis: for A being non empty set
for h, f being Element of PFuncs A,REAL holds
( h = (multrealpfunc A) . a,f iff ( dom h = dom f & ( for x being Element of A st x in dom f holds
h . x = a * (f . x) ) ) )
let A be non empty set ; :: thesis: for h, f being Element of PFuncs A,REAL holds
( h = (multrealpfunc A) . a,f iff ( dom h = dom f & ( for x being Element of A st x in dom f holds
h . x = a * (f . x) ) ) )
let h, f be Element of PFuncs A,REAL ; :: thesis: ( h = (multrealpfunc A) . a,f iff ( dom h = dom f & ( for x being Element of A st x in dom f holds
h . x = a * (f . x) ) ) )

hereby :: thesis: ( dom h = dom f & ( for x being Element of A st x in dom f holds
h . x = a * (f . x) ) implies h = (multrealpfunc A) . a,f )

assume A0: h = (multrealpfunc A) . a,f ; :: thesis: ( dom h = dom f & ( for x being Element of A st x in dom f holds
h . x = a * (f . x) ) )
then dom h = dom (a (#) f) by Def4;
hence dom h = dom f by VALUED_1:def 5; :: thesis: for x being Element of A st x in dom f holds
h . x = a * (f . x)
let x be Element of A; :: thesis: ( x in dom f implies h . x = a * (f . x) )
assume x in dom f ; :: thesis: h . x = a * (f . x)
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 A0, Def4; :: thesis: verum

end;

hereby :: thesis: verum

assume A1: ( dom f = dom h & ( for x being Element of A st x in dom f holds
h . x = a * (f . x) ) ) ; :: thesis: h = (multrealpfunc A) . a,f
reconsider k = (multrealpfunc A) . a,f as Element of PFuncs A,REAL ;

A2: now

let x be Element of A; :: thesis: ( x in dom f implies k . x = h . x )
assume A3: x in dom f ; :: thesis: k . x = h . x
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 A1, A3;
hence k . x = h . x by Def4; :: thesis: verum

end;

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

end;