let r, p be Complex; :: thesis: for seq being Complex_Sequence holds (r * p) (#) seq = r (#) (p (#) seq)
let seq be Complex_Sequence; :: thesis: (r * p) (#) seq = r (#) (p (#) seq)

now :: thesis: for n being Element of NAT holds ((r * p) (#) seq) . n = (r (#) (p (#) seq)) . n

let n be Element of NAT ; :: thesis: ((r * p) (#) seq) . n = (r (#) (p (#) seq)) . n
thus ((r * p) (#) seq) . n = (r * p) * (seq . n) by VALUED_1:6
.= r * (p * (seq . n))
.= r * ((p (#) seq) . n) by VALUED_1:6
.= (r (#) (p (#) seq)) . n by VALUED_1:6 ; :: thesis: verum

end;

hence (r * p) (#) seq = r (#) (p (#) seq) by FUNCT_2:63; :: thesis: verum