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