let C be non empty set ; :: thesis: for r, p being Real
for V being non empty scalar-associative RLSStruct
for f being PartFunc of C,V holds (r * p) (#) f = r (#) (p (#) f)
let r, p be Real; :: thesis: for V being non empty scalar-associative RLSStruct
for f being PartFunc of C,V holds (r * p) (#) f = r (#) (p (#) f)
let V be non empty scalar-associative RLSStruct ; :: thesis: for f being PartFunc of C,V holds (r * p) (#) f = r (#) (p (#) f)
let f be PartFunc of C,V; :: 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 :: thesis: for c being Element of C st c in dom ((r * p) (#) f) holds
((r * p) (#) f) /. c = (r (#) (p (#) f)) /. c

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 7
.= 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:1; :: thesis: verum