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 (<i> (#) f) = dom f by VALUED_1:def 5;
A3: dom (Im f) = dom f by COMSEQ_3:def 4;
A4: dom (Re (<i> (#) f)) = dom (<i> (#) f) by COMSEQ_3:def 3;

now :: thesis: for x being object st x in dom (- (Im f)) holds
(- (Im f)) . x = (Re (<i> (#) f)) . x

let x be object ; :: thesis: ( x in dom (- (Im f)) implies (- (Im f)) . x = (Re (<i> (#) f)) . x )
A5: (- (Im f)) . x = - ((Im f) . x) by VALUED_1:8;
A6: Re (<i> * (f . x)) = ((Re <i>) * (Re (f . x))) - ((Im <i>) * (Im (f . x))) by COMPLEX1:9;
assume A7: x in dom (- (Im f)) ; :: thesis: (- (Im f)) . x = (Re (<i> (#) f)) . x
then (Re (<i> (#) f)) . x = Re ((<i> (#) f) . x) by A1, A4, A2, A3, COMSEQ_3:def 3;
then (Re (<i> (#) f)) . x = - (Im (f . x)) by A1, A2, A3, A7, A6, COMPLEX1:7, VALUED_1:def 5;
hence (- (Im f)) . x = (Re (<i> (#) f)) . x by A1, A7, A5, COMSEQ_3:def 4; :: thesis: verum

end;

hence - (Im f) = Re (<i> (#) f) by A4, A2, A3, FUNCT_1:2, VALUED_1:8; :: thesis: Re f = Im (<i> (#) f)
A8: dom (Re f) = dom f by COMSEQ_3:def 3;
A9: dom (Im (<i> (#) f)) = dom (<i> (#) f) by COMSEQ_3:def 4;

now :: thesis: for x being object st x in dom (Re f) holds
(Re f) . x = (Im (<i> (#) f)) . x

let x be object ; :: thesis: ( x in dom (Re f) implies (Re f) . x = (Im (<i> (#) f)) . x )
A10: Im (<i> * (f . x)) = ((Im <i>) * (Re (f . x))) + ((Re <i>) * (Im (f . x))) by COMPLEX1:9;
assume A11: x in dom (Re f) ; :: thesis: (Re f) . x = (Im (<i> (#) f)) . x
then (Im (<i> (#) f)) . x = Im ((<i> (#) f) . x) by A8, A2, A9, COMSEQ_3:def 4;
then (Im (<i> (#) f)) . x = Re (f . x) by A8, A2, A11, A10, COMPLEX1:7, VALUED_1:def 5;
hence (Re f) . x = (Im (<i> (#) f)) . x by A11, COMSEQ_3:def 3; :: thesis: verum

end;

hence Re f = Im (<i> (#) f) by A8, A2, A9, FUNCT_1:2; :: thesis: verum