let X be non empty complex-membered add-closed set ; :: thesis: for seq, seq1, seq2 being sequence of X holds
( seq = seq1 + seq2 iff for n being Element of NAT holds seq . n = (seq1 . n) + (seq2 . n) )
let seq, seq1, seq2 be sequence of X; :: thesis: ( seq = seq1 + seq2 iff for n being Element of NAT holds seq . n = (seq1 . n) + (seq2 . n) )
thus ( seq = seq1 + seq2 implies for n being Element of NAT holds seq . n = (seq1 . n) + (seq2 . n) ) :: thesis: ( ( for n being Element of NAT holds seq . n = (seq1 . n) + (seq2 . n) ) implies seq = seq1 + seq2 )

proof

assume A1: seq = seq1 + seq2 ; :: thesis: for n being Element of NAT holds seq . n = (seq1 . n) + (seq2 . n)
let n be Element of NAT ; :: thesis: seq . n = (seq1 . n) + (seq2 . n)
dom seq = NAT by FUNCT_2:def 1;
hence seq . n = (seq1 . n) + (seq2 . n) by A1, VALUED_1:def 1; :: thesis: verum

end;

A2: dom seq = NAT by FUNCT_2:def 1;
assume for n being Element of NAT holds seq . n = (seq1 . n) + (seq2 . n) ; :: thesis: seq = seq1 + seq2
then A3: for n being set st n in dom seq holds
seq . n = (seq1 . n) + (seq2 . n) by A2;
dom seq = NAT /\ NAT by FUNCT_2:def 1
.= NAT /\ (dom seq2) by FUNCT_2:def 1
.= (dom seq1) /\ (dom seq2) by FUNCT_2:def 1 ;
hence seq = seq1 + seq2 by A3, VALUED_1:def 1; :: thesis: verum