let seq be Real_Sequence; :: thesis: for h being PartFunc of REAL,REAL
for r being real number st rng seq c= dom h holds
(r (#) h) /* seq = r (#) (h /* seq)
let h be PartFunc of REAL,REAL; :: thesis: for r being real number st rng seq c= dom h holds
(r (#) h) /* seq = r (#) (h /* seq)
let r be real number ; :: thesis: ( rng seq c= dom h implies (r (#) h) /* seq = r (#) (h /* seq) )
assume A1: rng seq c= dom h ; :: thesis: (r (#) h) /* seq = r (#) (h /* seq)
then A2: rng seq c= dom (r (#) h) by VALUED_1:def 5;

now

let n be Element of NAT ; :: thesis: ((r (#) h) /* seq) . n = r * ((h /* seq) . n)
A3: seq . n in rng seq by VALUED_0:28;
thus ((r (#) h) /* seq) . n = (r (#) h) . (seq . n) by A2, FUNCT_2:108
.= r * (h . (seq . n)) by A2, A3, VALUED_1:def 5
.= r * ((h /* seq) . n) by A1, FUNCT_2:108 ; :: thesis: verum

end;

hence (r (#) h) /* seq = r (#) (h /* seq) by SEQ_1:9; :: thesis: verum