let seq1, seq2, seq3 be Real_Sequence; :: thesis: ( 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) ) :: thesis: ( ( for n being Nat holds seq1 . n = (seq2 . n) - (seq3 . n) ) implies seq1 = seq2 - seq3 )

thus ( seq1 = seq2 - seq3 implies for n being Nat holds seq1 . n = (seq2 . n) - (seq3 . n) ) :: thesis: ( ( for n being Nat holds seq1 . n = (seq2 . n) - (seq3 . n) ) implies seq1 = seq2 - seq3 )

proof

assume A2:
for n being Nat holds seq1 . n = (seq2 . n) - (seq3 . n)
; :: thesis: seq1 = seq2 - seq3
assume A1:
seq1 = seq2 - seq3
; :: thesis: for n being Nat holds seq1 . n = (seq2 . n) - (seq3 . n)

end;now :: thesis: for n being Nat holds seq1 . n = (seq2 . n) - (seq3 . n)

hence
for n being Nat holds seq1 . n = (seq2 . n) - (seq3 . n)
; :: thesis: verumlet n be Nat; :: thesis: seq1 . n = (seq2 . n) - (seq3 . n)

seq1 . n = (seq2 . n) + ((- seq3) . n) by A1, SEQ_1:7;

then seq1 . n = (seq2 . n) + (- (seq3 . n)) by SEQ_1:10;

hence seq1 . n = (seq2 . n) - (seq3 . n) ; :: thesis: verum

end;seq1 . n = (seq2 . n) + ((- seq3) . n) by A1, SEQ_1:7;

then seq1 . n = (seq2 . n) + (- (seq3 . n)) by SEQ_1:10;

hence seq1 . n = (seq2 . n) - (seq3 . n) ; :: thesis: verum

now :: thesis: for n being Nat holds seq1 . n = (seq2 . n) + ((- seq3) . n)

hence
seq1 = seq2 - seq3
by SEQ_1:7; :: thesis: verumlet n be Nat; :: thesis: 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 ; :: thesis: verum

end;thus seq1 . n = (seq2 . n) - (seq3 . n) by A2

.= (seq2 . n) + (- (seq3 . n))

.= (seq2 . n) + ((- seq3) . n) by SEQ_1:10 ; :: thesis: verum