let C be non empty set ; for r being Real
for V being non empty scalar-associative RLSStruct
for f1 being PartFunc of C,REAL
for f2 being PartFunc of C,V holds r (#) (f1 (#) f2) = f1 (#) (r (#) f2)
let r be Real; for V being non empty scalar-associative RLSStruct
for f1 being PartFunc of C,REAL
for f2 being PartFunc of C,V holds r (#) (f1 (#) f2) = f1 (#) (r (#) f2)
let V be non empty scalar-associative RLSStruct ; for f1 being PartFunc of C,REAL
for f2 being PartFunc of C,V holds r (#) (f1 (#) f2) = f1 (#) (r (#) f2)
let f1 be PartFunc of C,REAL; for f2 being PartFunc of C,V holds r (#) (f1 (#) f2) = f1 (#) (r (#) f2)
let f2 be PartFunc of C,V; r (#) (f1 (#) f2) = f1 (#) (r (#) f2)
A1: dom (r (#) (f1 (#) f2)) =
dom (f1 (#) f2)
by Def4
.=
(dom f1) /\ (dom f2)
by Def3
.=
(dom f1) /\ (dom (r (#) f2))
by Def4
.=
dom (f1 (#) (r (#) f2))
by Def3
;
hence
r (#) (f1 (#) f2) = f1 (#) (r (#) f2)
by A1, PARTFUN2:1; verum