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 MESFUN6C:def 1
.= dom (Re g) by AS, MESFUN6C:def 1 ;
P2: dom (Im f) = dom f by MESFUN6C:def 2
.= dom (Im g) by AS, MESFUN6C:def 2 ;

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
thus (Re f) . x = Re (f . x) by MESFUN6C:def 1, A1
.= (Re g) . x by AS, MESFUN6C:def 1, P1, 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
thus (Im f) . x = Im (f . x) by MESFUN6C:def 2, A1
.= (Im g) . x by AS, MESFUN6C:def 2, P2, 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