let seq1, seq2 be Real_Sequence; :: thesis: (seq1 + seq2) - seq2 = seq1
for n being Element of NAT holds ((seq1 + seq2) - seq2) . n = seq1 . n

proof

let n be Element of NAT ; :: thesis: ((seq1 + seq2) - seq2) . n = seq1 . n
((seq1 + seq2) - seq2) . n = (seq1 + (seq2 - seq2)) . n by SEQ_1:31
.= (seq1 . n) + ((seq2 + (- seq2)) . n) by SEQ_1:7
.= (seq1 . n) + ((seq2 . n) + ((- seq2) . n)) by SEQ_1:7
.= (seq1 . n) + ((seq2 . n) + (- (seq2 . n))) by SEQ_1:10
.= seq1 . n ;
hence ((seq1 + seq2) - seq2) . n = seq1 . n ; :: thesis: verum

end;

hence (seq1 + seq2) - seq2 = seq1 by FUNCT_2:63; :: thesis: verum