let seq1, seq2, seq3 be Real_Sequence; ( seq1 = seq2 - seq3 iff for n being Nat holds seq1 . n = (seq2 . n) - (seq3 . n) )
thus
( seq1 = seq2 - seq3 implies for n being Nat holds seq1 . n = (seq2 . n) - (seq3 . n) )
( ( for n being Nat holds seq1 . n = (seq2 . n) - (seq3 . n) ) implies seq1 = seq2 - seq3 )proof
assume A1:
seq1 = seq2 - seq3
;
for n being Nat holds seq1 . n = (seq2 . n) - (seq3 . n)
now for n being Nat holds seq1 . n = (seq2 . n) - (seq3 . n)end;
hence
for
n being
Nat holds
seq1 . n = (seq2 . n) - (seq3 . n)
;
verum
end;
assume A2:
for n being Nat holds seq1 . n = (seq2 . n) - (seq3 . n)
; seq1 = seq2 - seq3
now for n being Nat holds seq1 . n = (seq2 . n) + ((- seq3) . n)let n be
Nat;
seq1 . n = (seq2 . n) + ((- seq3) . n)thus seq1 . n =
(seq2 . n) - (seq3 . n)
by A2
.=
(seq2 . n) + (- (seq3 . n))
.=
(seq2 . n) + ((- seq3) . n)
by SEQ_1:10
;
verum end;
hence
seq1 = seq2 - seq3
by SEQ_1:7; verum