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