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