let f be PartFunc of REAL ,COMPLEX ; :: thesis: for A being non empty Subset of REAL
for g being Function of A,COMPLEX st f = g holds
( Re f = Re g & Im f = Im g )
let A be non empty Subset of REAL ; :: 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 ;

now

let x be set ; :: thesis: ( x in dom (Re f) implies (Re f) . x = (Re g) . x )
assume P10: x in dom (Re f) ; :: thesis: (Re f) . x = (Re g) . x
then reconsider x0 = x as Element of REAL ;
thus (Re f) . x = Re (f . x0) by P10, MESFUN6C:def 1
.= (Re g) . x by AS, P10, P1, MESFUN6C:def 1 ; :: thesis: verum

end;

hence Re f = Re g by P1, FUNCT_1:9; :: thesis: Im f = Im g
P2: dom (Im f) = dom f by MESFUN6C:def 2
.= dom (Im g) by AS, MESFUN6C:def 2 ;

now

let x be set ; :: thesis: ( x in dom (Im f) implies (Im f) . x = (Im g) . x )
assume P20: x in dom (Im f) ; :: thesis: (Im f) . x = (Im g) . x
then reconsider x0 = x as Element of REAL ;
thus (Im f) . x = Im (f . x0) by P20, MESFUN6C:def 2
.= (Im g) . x by AS, P20, P2, MESFUN6C:def 2 ; :: thesis: verum

end;

hence Im f = Im g by P2, FUNCT_1:9; :: thesis: verum