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 A1: f = g ; :: thesis: ( Re f = Re g & Im f = Im g )
A2: dom (Re f) = dom f by COMSEQ_3:def 3
.= dom (Re g) by A1, COMSEQ_3:def 3 ;
A3: dom (Im f) = dom f by COMSEQ_3:def 4
.= dom (Im g) by A1, COMSEQ_3:def 4 ;

A4: now

let x be set ; :: thesis: ( x in dom (Re f) implies (Re f) . x = (Re g) . x )
assume A5: 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 A1, A5, COMSEQ_3:def 3 ;
:: thesis: verum

end;

A6: now

let x be set ; :: thesis: ( x in dom (Im f) implies (Im f) . x = (Im g) . x )
assume A7: 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 A1, A7, COMSEQ_3:def 4 ;
:: thesis: verum

end;

thus Re f = Re g by A2, A4, FUNCT_1:2; :: thesis: Im f = Im g
thus Im f = Im g by A3, A6, FUNCT_1:2; :: thesis: verum