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 A1: 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) ;
A2: dom f = dom aG by A1, VFUNCT_1:def 4;
A5: a (#) f = f [#] a by INTEGR15:def 11;
for c being set st c in dom aG holds
aG . c = a (#) (f . c)

proof

let c be set ; :: thesis: ( c in dom aG implies aG . c = a (#) (f . c) )
assume A7: c in dom aG ; :: thesis: aG . c = a (#) (f . c)
then A3: c in dom (a (#) g) ;
A4: f /. c = g /. c by A1, REAL_NS1:def 4;
A6: f /. c = f . c by A2, A7, PARTFUN1:def 6;
aG . c = (a (#) g) /. c by A7, PARTFUN1:def 6
.= a * (g /. c) by A3, VFUNCT_1:def 4 ;
hence aG . c = a (#) (f . c) by A4, A6, REAL_NS1:3; :: thesis: verum

end;

hence a (#) f = a (#) g by A2, A5, VALUED_2:def 39; :: thesis: verum