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

now

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

end;

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