let seq1, seq2 be Complex_Sequence; :: thesis: ( Re seq1 = Re seq2 & Im seq1 = Im seq2 implies seq1 = seq2 )
assume that
A1: Re seq1 = Re seq2 and
A2: Im seq1 = Im seq2 ; :: thesis: seq1 = seq2

now :: thesis: for n being Element of NAT holds seq1 . n = seq2 . n

let n be Element of NAT ; :: thesis: seq1 . n = seq2 . n
A3: Im (seq1 . n) = (Im seq2) . n by A2, Def6
.= Im (seq2 . n) by Def6 ;
Re (seq1 . n) = (Re seq2) . n by A1, Def5
.= Re (seq2 . n) by Def5 ;
hence seq1 . n = seq2 . n by A3, COMPLEX1:3; :: thesis: verum

end;

hence seq1 = seq2 ; :: thesis: verum