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