let seq, seq1, 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 Th15
.= (seq1 + seq19) /" seq ; :: thesis: (seq1 /" seq) - (seq19 /" seq) = (seq1 - seq19) /" seq
thus (seq1 /" seq) - (seq19 /" seq) = (seq1 - seq19) (#) (seq ") by Th20
.= (seq1 - seq19) /" seq ; :: thesis: verum