let n, m be 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;
A3: a (#) f = f [#] a by INTEGR15:def 11;
for c being object st c in dom aG holds
aG . c = a (#) (f . c)

proof

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

end;

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