let X be non empty set ; :: thesis: for S being SigmaField of X

for f being PartFunc of X,COMPLEX

for A being Element of S holds

( (Re f) | A = Re (f | A) & (Im f) | A = Im (f | A) )

let S be SigmaField of X; :: thesis: for f being PartFunc of X,COMPLEX

for A being Element of S holds

( (Re f) | A = Re (f | A) & (Im f) | A = Im (f | A) )

let f be PartFunc of X,COMPLEX; :: thesis: for A being Element of S holds

( (Re f) | A = Re (f | A) & (Im f) | A = Im (f | A) )

let A be Element of S; :: 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 ;

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 ;

for f being PartFunc of X,COMPLEX

for A being Element of S holds

( (Re f) | A = Re (f | A) & (Im f) | A = Im (f | A) )

let S be SigmaField of X; :: thesis: for f being PartFunc of X,COMPLEX

for A being Element of S holds

( (Re f) | A = Re (f | A) & (Im f) | A = Im (f | A) )

let f be PartFunc of X,COMPLEX; :: thesis: for A being Element of S holds

( (Re f) | A = Re (f | A) & (Im f) | A = Im (f | A) )

let A be Element of S; :: 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

hence
(Re f) | A = Re (f | A)
by A1, FUNCT_1:2; :: thesis: (Im f) | A = Im (f | A)(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 A3, XBOOLE_0:def 4;

thus (Re (f | A)) . x = Re ((f | A) . x) by A1, A2, COMSEQ_3:def 3

.= Re (f . x) by A5, FUNCT_1:49

.= (Re f) . x by A4, COMSEQ_3:def 3

.= ((Re f) | A) . x by A5, FUNCT_1:49 ; :: thesis: verum

end;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 A3, XBOOLE_0:def 4;

thus (Re (f | A)) . x = Re ((f | A) . x) by A1, A2, COMSEQ_3:def 3

.= Re (f . x) by A5, FUNCT_1:49

.= (Re f) . x by A4, COMSEQ_3:def 3

.= ((Re f) | A) . x by A5, FUNCT_1:49 ; :: thesis: verum

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

hence
(Im f) | A = Im (f | A)
by A6, FUNCT_1:2; :: thesis: verum(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 A8, XBOOLE_0:def 4;

thus (Im (f | A)) . x = Im ((f | A) . x) by A6, A7, COMSEQ_3:def 4

.= Im (f . x) by A10, FUNCT_1:49

.= (Im f) . x by A9, COMSEQ_3:def 4

.= ((Im f) | A) . x by A10, FUNCT_1:49 ; :: thesis: verum

end;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 A8, XBOOLE_0:def 4;

thus (Im (f | A)) . x = Im ((f | A) . x) by A6, A7, COMSEQ_3:def 4

.= Im (f . x) by A10, FUNCT_1:49

.= (Im f) . x by A9, COMSEQ_3:def 4

.= ((Im f) | A) . x by A10, FUNCT_1:49 ; :: thesis: verum