let seq, seq1, seq2 be Complex_Sequence; :: thesis: seq2 (#) (seq1 /" seq) = (seq2 (#) seq1) /" seq
thus seq2 (#) (seq1 /" seq) = (seq2 (#) seq1) (#) (seq ") by Th8
.= (seq2 (#) seq1) /" seq ; :: thesis: verum