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