let n be Element of NAT ; :: thesis: for f1 being PartFunc of REAL, the carrier of (REAL-NS n)
for g1 being PartFunc of REAL,(REAL n)
for a being Real st f1 = g1 holds
a (#) f1 = a (#) g1
let f1 be PartFunc of REAL, the carrier of (REAL-NS n); :: thesis: for g1 being PartFunc of REAL,(REAL n)
for a being Real st f1 = g1 holds
a (#) f1 = a (#) g1
let g1 be PartFunc of REAL,(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 AS: f1 = g1 ; :: thesis: a (#) f1 = a (#) g1
S: dom (a (#) f1) = dom f1 by VFUNCT_1:def 4;
then A2: dom (a (#) f1) = dom (a (#) g1) by AS, VALUED_2:def 39;

B1: now

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

end;

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