let m, n be Element of NAT ; :: thesis: for f being PartFunc of (REAL m),(REAL n)
for g being PartFunc of (REAL-NS m),(REAL-NS n)
for a being Real st f = g holds
a (#) f = a (#) g
let f be PartFunc of (REAL m),(REAL n); :: thesis: for g being PartFunc of (REAL-NS m),(REAL-NS n)
for a being Real st f = g holds
a (#) f = a (#) g
let g be PartFunc of (REAL-NS m),(REAL-NS n); :: thesis: for a being Real st f = g holds
a (#) f = a (#) g
let a be Real; :: thesis: ( f = g implies a (#) f = a (#) g )
assume AS: f = g ; :: thesis: a (#) f = a (#) g
( the carrier of (REAL-NS m) = REAL m & the carrier of (REAL-NS n) = REAL n ) by REAL_NS1:def 4;
then reconsider aG = a (#) g as PartFunc of (REAL m),(REAL n) ;
P1: dom f = dom aG by AS, VFUNCT_1:def 4;
for c being Element of REAL m st c in dom aG holds
aG /. c = a * (f /. c)

proof

let c be Element of REAL m; :: thesis: ( c in dom aG implies aG /. c = a * (f /. c) )
assume c in dom aG ; :: thesis: aG /. c = a * (f /. c)
then P21: c in dom (a (#) g) ;
P22: f /. c = g /. c by AS, REAL_NS1:def 4;
aG /. c = (a (#) g) /. c by REAL_NS1:def 4
.= a * (g /. c) by P21, VFUNCT_1:def 4 ;
hence aG /. c = a * (f /. c) by P22, REAL_NS1:3; :: thesis: verum

end;

hence a (#) f = a (#) g by P1, INTEGR15:def 11; :: thesis: verum