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

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

let x be object ; :: thesis: ( x in dom ((Re f) + (<i> (#) (Im f))) implies ((Re f) + (<i> (#) (Im f))) . x = f . x )
assume A5: 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 A1, A3, A5, COMSEQ_3:def 3
.= (Re (f . x)) + (<i> * ((Im f) . x)) by A2, A4, A3, A5, VALUED_1:def 5
.= (Re (f . x)) + (<i> * (Im (f . x))) by A2, A3, A5, COMSEQ_3:def 4 ;
hence ((Re f) + (<i> (#) (Im f))) . x = f . x by COMPLEX1:13; :: thesis: verum

end;

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