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