let seq, seq9 be Complex_Sequence; :: thesis: |.(seq9 /" seq).| = |.seq9.| /" |.seq.|
thus |.(seq9 /" seq).| = |.seq9.| (#) |.(seq ").| by Th45
.= |.seq9.| /" |.seq.| by Th46 ; :: thesis: verum