let r be Element of COMPLEX ; :: thesis: for seq1, seq being Complex_Sequence holds r (#) (seq1 /" seq) = (r (#) seq1) /" seq
let seq1, seq be Complex_Sequence; :: thesis: r (#) (seq1 /" seq) = (r (#) seq1) /" seq
thus r (#) (seq1 /" seq) = r (#) (seq1 (#) (seq "))
.= (r (#) seq1) /" seq by Th15 ; :: thesis: verum