let C be non empty set ; :: thesis: for V being RealNormSpace
for f being PartFunc of C,the carrier of V
for r, p being Real holds (r * p) (#) f = r (#) (p (#) f)
let V be RealNormSpace; :: thesis: for f being PartFunc of C,the carrier of V
for r, p being Real holds (r * p) (#) f = r (#) (p (#) f)
let f be PartFunc of C,the carrier of V; :: thesis: for r, p being Real holds (r * p) (#) f = r (#) (p (#) f)
let r, p be Real; :: thesis: (r * p) (#) f = r (#) (p (#) f)
A1: dom ((r * p) (#) f) = dom f by Def4
.= dom (p (#) f) by Def4
.= dom (r (#) (p (#) f)) by Def4 ;

now

let c be Element of C; :: thesis: ( c in dom ((r * p) (#) f) implies ((r * p) (#) f) /. c = (r (#) (p (#) f)) /. c )
assume A2: c in dom ((r * p) (#) f) ; :: thesis: ((r * p) (#) f) /. c = (r (#) (p (#) f)) /. c
then A3: c in dom (p (#) f) by A1, Def4;
thus ((r * p) (#) f) /. c = (r * p) * (f /. c) by A2, Def4
.= r * (p * (f /. c)) by RLVECT_1:def 9
.= r * ((p (#) f) /. c) by A3, Def4
.= (r (#) (p (#) f)) /. c by A1, A2, Def4 ; :: thesis: verum

end;

hence (r * p) (#) f = r (#) (p (#) f) by A1, PARTFUN2:3; :: thesis: verum