let a, b be Real_Sequence; :: thesis: a = (a + b) - b

now :: thesis: for n being Element of NAT holds ((a + b) - b) . n = a . n

let n be Element of NAT ; :: thesis: ((a + b) - b) . n = a . n
(a + (b + (- b))) . n = (a . n) + ((b + (- b)) . n) by SEQ_1:7
.= (a . n) + ((b . n) + ((- b) . n)) by SEQ_1:7
.= (a . n) + ((b . n) + (- (b . n))) by SEQ_1:10
.= a . n ;
hence ((a + b) - b) . n = a . n by SEQ_1:13; :: thesis: verum

end;

hence a = (a + b) - b by FUNCT_2:63; :: thesis: verum