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

hence
a = (a + b) - b
by FUNCT_2:63; :: thesis: verumlet 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;(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