let r be Complex; :: thesis: for seq, seq1 being Complex_Sequence holds r (#) (seq1 /" seq) = (r (#) seq1) /" seq
let seq, seq1 be Complex_Sequence; :: thesis: r (#) (seq1 /" seq) = (r (#) seq1) /" seq
thus r (#) (seq1 /" seq) = r (#) (seq1 (#) (seq "))
.= (r (#) seq1) /" seq by Th12 ; :: thesis: verum