let X be non empty set ; :: thesis: for f being PartFunc of X,COMPLEX
for A being set holds
( (Re f) | A = Re (f | A) & (Im f) | A = Im (f | A) )
let f be PartFunc of X,COMPLEX ; :: thesis: for A being set holds
( (Re f) | A = Re (f | A) & (Im f) | A = Im (f | A) )
let A be set ; :: thesis: ( (Re f) | A = Re (f | A) & (Im f) | A = Im (f | A) )
dom ((Re f) | A) = (dom (Re f)) /\ A by RELAT_1:90
.= (dom f) /\ A by MESFUN6C:def 1 ;
then A1: dom ((Re f) | A) = dom (f | A) by RELAT_1:90
.= dom (Re (f | A)) by MESFUN6C:def 1 ;

now

let x be set ; :: thesis: ( x in dom ((Re f) | A) implies (Re (f | A)) . x = ((Re f) | A) . x )
assume A2: x in dom ((Re f) | A) ; :: thesis: (Re (f | A)) . x = ((Re f) | A) . x
then x in (dom (Re f)) /\ A by RELAT_1:90;
then A3: ( x in dom (Re f) & x in A ) by XBOOLE_0:def 4;
thus (Re (f | A)) . x = Re ((f | A) . x) by A1, A2, MESFUN6C:def 1
.= Re (f . x) by A3, FUNCT_1:72
.= (Re f) . x by A3, MESFUN6C:def 1
.= ((Re f) | A) . x by A3, FUNCT_1:72 ; :: thesis: verum

end;

hence (Re f) | A = Re (f | A) by A1, FUNCT_1:9; :: thesis: (Im f) | A = Im (f | A)
dom ((Im f) | A) = (dom (Im f)) /\ A by RELAT_1:90;
then dom ((Im f) | A) = (dom f) /\ A by MESFUN6C:def 2;
then B1: dom ((Im f) | A) = dom (f | A) by RELAT_1:90
.= dom (Im (f | A)) by MESFUN6C:def 2 ;

now

let x be set ; :: thesis: ( x in dom ((Im f) | A) implies (Im (f | A)) . x = ((Im f) | A) . x )
assume B2: x in dom ((Im f) | A) ; :: thesis: (Im (f | A)) . x = ((Im f) | A) . x
then x in (dom (Im f)) /\ A by RELAT_1:90;
then B3: ( x in dom (Im f) & x in A ) by XBOOLE_0:def 4;
thus (Im (f | A)) . x = Im ((f | A) . x) by B1, B2, MESFUN6C:def 2
.= Im (f . x) by B3, FUNCT_1:72
.= (Im f) . x by B3, MESFUN6C:def 2
.= ((Im f) | A) . x by B3, FUNCT_1:72 ; :: thesis: verum

end;

hence (Im f) | A = Im (f | A) by B1, FUNCT_1:9; :: thesis: verum