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