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

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

end;

hence seq1 = seq2 by FUNCT_2:113; :: thesis: verum