let seq1, seq, seq1' be Real_Sequence; :: thesis: ( (seq1 /" seq) + (seq1' /" seq) = (seq1 + seq1') /" seq & (seq1 /" seq) - (seq1' /" seq) = (seq1 - seq1') /" seq )
thus (seq1 /" seq) + (seq1' /" seq) = (seq1 + seq1') (#) (seq " ) by Th23
.= (seq1 + seq1') /" seq ; :: thesis: (seq1 /" seq) - (seq1' /" seq) = (seq1 - seq1') /" seq
thus (seq1 /" seq) - (seq1' /" seq) = (seq1 - seq1') (#) (seq " ) by Th28
.= (seq1 - seq1') /" seq ; :: thesis: verum