let X be non empty set ; :: thesis: for f being PartFunc of X,COMPLEX holds
( - (Im f) = Re (<i> (#) f) & Re f = Im (<i> (#) f) )
let f be PartFunc of X,COMPLEX ; :: thesis: ( - (Im f) = Re (<i> (#) f) & Re f = Im (<i> (#) f) )
A1: dom (- (Im f)) = dom (Im f) by VALUED_1:8;
A2: ( dom (Re (<i> (#) f)) = dom (<i> (#) f) & dom (Re f) = dom f ) by Def1;
A3: dom (<i> (#) f) = dom f by VALUED_1:def 5;
A5: ( dom (Im (<i> (#) f)) = dom (<i> (#) f) & dom (Im f) = dom f ) by Def2;

now

let x be set ; :: thesis: ( x in dom (- (Im f)) implies (- (Im f)) . x = (Re (<i> (#) f)) . x )
assume P01: x in dom (- (Im f)) ; :: thesis: (- (Im f)) . x = (Re (<i> (#) f)) . x
then P06: (Re (<i> (#) f)) . x = Re ((<i> (#) f) . x) by A1, A2, A3, A5, Def1;
Q01: (- (Im f)) . x = - ((Im f) . x) by VALUED_1:8;
Re (<i> * (f . x)) = ((Re <i> ) * (Re (f . x))) - ((Im <i> ) * (Im (f . x))) by COMPLEX1:24;
then (Re (<i> (#) f)) . x = - (Im (f . x)) by P06, P01, A1, A3, A5, COMPLEX1:17, VALUED_1:def 5;
hence (- (Im f)) . x = (Re (<i> (#) f)) . x by Q01, P01, A1, Def2; :: thesis: verum

end;

hence - (Im f) = Re (<i> (#) f) by A2, A3, A5, FUNCT_1:9, VALUED_1:8; :: thesis: Re f = Im (<i> (#) f)

now

let x be set ; :: thesis: ( x in dom (Re f) implies (Re f) . x = (Im (<i> (#) f)) . x )
assume P01: x in dom (Re f) ; :: thesis: (Re f) . x = (Im (<i> (#) f)) . x
then P06: (Im (<i> (#) f)) . x = Im ((<i> (#) f) . x) by A2, A3, A5, Def2;
Im (<i> * (f . x)) = ((Im <i> ) * (Re (f . x))) + ((Re <i> ) * (Im (f . x))) by COMPLEX1:24;
then (Im (<i> (#) f)) . x = Re (f . x) by P06, P01, A2, A3, COMPLEX1:17, VALUED_1:def 5;
hence (Re f) . x = (Im (<i> (#) f)) . x by P01, Def1; :: thesis: verum

end;

hence Re f = Im (<i> (#) f) by A2, A3, A5, FUNCT_1:9; :: thesis: verum