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