let n be Element of NAT ; 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 ; 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); 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); for a being Real st f1 = g1 holds
a (#) f1 = a (#) g1
let a be Real; ( f1 = g1 implies a (#) f1 = a (#) g1 )
assume A1:
f1 = g1
; 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 for x being Element of W st x in dom (a (#) f1) holds
(a (#) f1) . x = (a (#) g1) . xlet x be
Element of
W;
( x in dom (a (#) f1) implies (a (#) f1) . x = (a (#) g1) . x )assume A5:
x in dom (a (#) f1)
;
(a (#) f1) . x = (a (#) g1) . xthen 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;
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; verum