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 )
proof
assume A1: seq1 = seq2 - seq3 ; :: thesis: for n being Nat holds seq1 . n = (seq2 . n) - (seq3 . n)
now :: thesis: for n being Nat holds seq1 . n = (seq2 . n) - (seq3 . n)
let 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;
hence for n being Nat holds seq1 . n = (seq2 . n) - (seq3 . n) ; :: thesis: verum
end;
assume A2: for n being Nat holds seq1 . n = (seq2 . n) - (seq3 . n) ; :: thesis: seq1 = seq2 - seq3
now :: thesis: for n being Nat holds seq1 . n = (seq2 . n) + ((- seq3) . n)
let 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;
hence seq1 = seq2 - seq3 by SEQ_1:7; :: thesis: verum