let seq1, seq2, seq3 be Complex_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)
A2: n in NAT by ORDINAL1:def 12;
seq1 . n = (seq2 . n) + ((- seq3) . n) by A1, VALUED_1:1, A2;
then seq1 . n = (seq2 . n) + (- (seq3 . n)) by VALUED_1:8;
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 A3: for n being Nat holds seq1 . n = (seq2 . n) - (seq3 . n) ; :: thesis: seq1 = seq2 - seq3

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

let n be Element of NAT ; :: thesis: seq1 . n = (seq2 + (- seq3)) . n
thus seq1 . n = (seq2 . n) - (seq3 . n) by A3
.= (seq2 . n) + (- (seq3 . n))
.= (seq2 . n) + ((- seq3) . n) by VALUED_1:8
.= (seq2 + (- seq3)) . n by VALUED_1:1 ; :: thesis: verum

end;

hence seq1 = seq2 - seq3 by FUNCT_2:63; :: thesis: verum