let X be non empty set ; for f being PartFunc of X,COMPLEX holds f = (Re f) + (<i> (#) (Im f))
let f be PartFunc of X,COMPLEX; 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 for x being object st x in dom ((Re f) + (<i> (#) (Im f))) holds
((Re f) + (<i> (#) (Im f))) . x = f . xlet x be
object ;
( 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)))
;
((Re f) + (<i> (#) (Im f))) . x = f . xthen ((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;
verum end;
hence
f = (Re f) + (<i> (#) (Im f))
by A3, FUNCT_1:2; verum