let n be Element of NAT ; :: thesis: for W being non empty set
for f1 being PartFunc of W,(REAL-NS n)
for g1 being PartFunc of W,(REAL n)
for a being Real st f1 = g1 holds
a (#) f1 = a (#) g1
let W be non empty set ; :: thesis: for f1 being PartFunc of W,(REAL-NS n)
for g1 being PartFunc of W,(REAL n)
for a being Real st f1 = g1 holds
a (#) f1 = a (#) g1
let f1 be PartFunc of W,(REAL-NS n); :: thesis: for g1 being PartFunc of W,(REAL n)
for a being Real st f1 = g1 holds
a (#) f1 = a (#) g1
let g1 be PartFunc of W,(REAL n); :: thesis: for a being Real st f1 = g1 holds
a (#) f1 = a (#) g1
let a be Real; :: thesis: ( f1 = g1 implies a (#) f1 = a (#) g1 )
assume A1: f1 = g1 ; :: thesis: a (#) f1 = a (#) g1
A2: dom (a (#) f1) = dom f1 by VFUNCT_1:def 4;
then A3: dom (a (#) f1) = dom (a (#) g1) by A1, VALUED_2:def 39;

A4: now :: thesis: for x being Element of W st x in dom (a (#) f1) holds
(a (#) f1) . x = (a (#) g1) . x

let x be Element of W; :: thesis: ( x in dom (a (#) f1) implies (a (#) f1) . x = (a (#) g1) . x )
assume A5: x in dom (a (#) f1) ; :: thesis: (a (#) f1) . x = (a (#) g1) . x
then A6: g1 . x = g1 /. x by A1, A2, PARTFUN1:def 6;
f1 /. x = g1 /. x by A1, REAL_NS1:def 4;
then A7: a * (f1 /. x) = a * (g1 /. x) by REAL_NS1:3;
A8: (a (#) f1) /. x = a * (f1 /. x) by A5, VFUNCT_1:def 4;
(a (#) g1) . x = a (#) (g1 . x) by A3, A5, VALUED_2:def 39;
hence (a (#) f1) . x = (a (#) g1) . x by A5, A7, A8, A6, PARTFUN1:def 6; :: thesis: verum

end;

a (#) f1 is PartFunc of W,(REAL n) by REAL_NS1:def 4;
hence a (#) f1 = a (#) g1 by A3, A4, PARTFUN1:5; :: thesis: verum