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