let f be PartFunc of REAL,COMPLEX; :: thesis: for A being Subset of REAL holds
( Re (f | A) = (Re f) | A & Im (f | A) = (Im f) | A )

let A be Subset of REAL; :: thesis: ( Re (f | A) = (Re f) | A & Im (f | A) = (Im f) | A )
dom ((Re f) | A) = (dom (Re f)) /\ A by RELAT_1:61
.= (dom f) /\ A by COMSEQ_3:def 3 ;
then A1: dom ((Re f) | A) = dom (f | A) by RELAT_1:61
.= dom (Re (f | A)) by COMSEQ_3:def 3 ;
now :: thesis: for x being object st x in dom ((Re f) | A) holds
(Re (f | A)) . x = ((Re f) | A) . x
let x be object ; :: 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 A3: x in (dom (Re f)) /\ A by RELAT_1:61;
then A4: x in dom (Re f) by XBOOLE_0:def 4;
A5: x in A by ;
thus (Re (f | A)) . x = Re ((f | A) . x) by
.= Re (f . x) by
.= (Re f) . x by
.= ((Re f) | A) . x by ; :: thesis: verum
end;
hence (Re f) | A = Re (f | A) by ; :: thesis: Im (f | A) = (Im f) | A
dom ((Im f) | A) = (dom (Im f)) /\ A by RELAT_1:61
.= (dom f) /\ A by COMSEQ_3:def 4 ;
then A6: dom ((Im f) | A) = dom (f | A) by RELAT_1:61
.= dom (Im (f | A)) by COMSEQ_3:def 4 ;
now :: thesis: for x being object st x in dom ((Im f) | A) holds
(Im (f | A)) . x = ((Im f) | A) . x
let x be object ; :: thesis: ( x in dom ((Im f) | A) implies (Im (f | A)) . x = ((Im f) | A) . x )
assume A7: x in dom ((Im f) | A) ; :: thesis: (Im (f | A)) . x = ((Im f) | A) . x
then A8: x in (dom (Im f)) /\ A by RELAT_1:61;
then A9: x in dom (Im f) by XBOOLE_0:def 4;
A10: x in A by ;
thus (Im (f | A)) . x = Im ((f | A) . x) by
.= Im (f . x) by
.= (Im f) . x by
.= ((Im f) | A) . x by ; :: thesis: verum
end;
hence Im (f | A) = (Im f) | A by ; :: thesis: verum