let A be non empty Subset of REAL ; :: thesis: for f being PartFunc of REAL ,COMPLEX
for g being Function of A,COMPLEX st f = g holds
( Re f = Re g & Im f = Im g )
let f be PartFunc of REAL ,COMPLEX ; :: thesis: for g being Function of A,COMPLEX st f = g holds
( Re f = Re g & Im f = Im g )
let g be Function of A,COMPLEX ; :: thesis: ( f = g implies ( Re f = Re g & Im f = Im g ) )
assume AS: f = g ; :: thesis: ( Re f = Re g & Im f = Im g )
P1: dom (Re f) = dom f by COMSEQ_3:def 3
.= dom (Re g) by AS, COMSEQ_3:def 3 ;
P2: dom (Im f) = dom f by COMSEQ_3:def 4
.= dom (Im g) by AS, COMSEQ_3:def 4 ;

Q1: now

let x be set ; :: thesis: ( x in dom (Re f) implies (Re f) . x = (Re g) . x )
assume A1: x in dom (Re f) ; :: thesis: (Re f) . x = (Re g) . x
hence (Re f) . x = Re (f . x) by COMSEQ_3:def 3
.= (Re g) . x by AS, COMSEQ_3:def 3, A1 ;
:: thesis: verum

end;

Q2: now

let x be set ; :: thesis: ( x in dom (Im f) implies (Im f) . x = (Im g) . x )
assume A1: x in dom (Im f) ; :: thesis: (Im f) . x = (Im g) . x
hence (Im f) . x = Im (f . x) by COMSEQ_3:def 4
.= (Im g) . x by AS, COMSEQ_3:def 4, A1 ;
:: thesis: verum

end;

thus Re f = Re g by P1, Q1, FUNCT_1:9; :: thesis: Im f = Im g
thus Im f = Im g by P2, Q2, FUNCT_1:9; :: thesis: verum