let r be Complex; :: thesis: for seq1, seq2 being Complex_Sequence holds r (#) (seq1 (#) seq2) = seq1 (#) (r (#) seq2)
let seq1, seq2 be Complex_Sequence; :: thesis: r (#) (seq1 (#) seq2) = seq1 (#) (r (#) seq2)

now :: thesis: for n being Element of NAT holds (r (#) (seq1 (#) seq2)) . n = (seq1 (#) (r (#) seq2)) . n

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

end;

hence r (#) (seq1 (#) seq2) = seq1 (#) (r (#) seq2) by FUNCT_2:63; :: thesis: verum