let f be complex-valued Sequence; :: thesis: for n being Nat holds
( Re (Shift (f,n)) = Shift ((Re f),n) & Im (Shift (f,n)) = Shift ((Im f),n) )
let n be Nat; :: thesis: ( Re (Shift (f,n)) = Shift ((Re f),n) & Im (Shift (f,n)) = Shift ((Im f),n) )
A0: ( dom (Re (Shift (f,n))) = dom (Shift (f,n)) & dom (Re f) = dom f ) by COMSEQ_3:def 3;
then A1: dom (Re (Shift (f,n))) = { (m + n) where m is Nat : m in dom f } by VALUED_1:def 12
.= dom (Shift ((Re f),n)) by A0, VALUED_1:def 12 ;
A0a: ( dom (Im (Shift (f,n))) = dom (Shift (f,n)) & dom (Im f) = dom f ) by COMSEQ_3:def 4;
then A2: dom (Im (Shift (f,n))) = { (m + n) where m is Nat : m in dom f } by VALUED_1:def 12
.= dom (Shift ((Im f),n)) by A0a, VALUED_1:def 12 ;
A3: for x being object st x in dom (Re (Shift (f,n))) holds
(Re (Shift (f,n))) . x = (Shift ((Re f),n)) . x

proof

let x be object ; :: thesis: ( x in dom (Re (Shift (f,n))) implies (Re (Shift (f,n))) . x = (Shift ((Re f),n)) . x )
assume B1: x in dom (Re (Shift (f,n))) ; :: thesis: (Re (Shift (f,n))) . x = (Shift ((Re f),n)) . x
then consider k being Nat such that
B2: ( k in dom f & x = k + n ) by A0, VALUED_1:39;
(Re (Shift (f,n))) . x = Re ((Shift (f,n)) . (k + n)) by B1, B2, COMSEQ_3:def 3
.= Re (f . k) by B2, VALUED_1:def 12
.= (Re f) . k by A0, B2, COMSEQ_3:def 3
.= (Shift ((Re f),n)) . (k + n) by A0, B2, VALUED_1:def 12 ;
hence (Re (Shift (f,n))) . x = (Shift ((Re f),n)) . x by B2; :: thesis: verum

end;

for x being object st x in dom (Im (Shift (f,n))) holds
(Im (Shift (f,n))) . x = (Shift ((Im f),n)) . x

proof

let x be object ; :: thesis: ( x in dom (Im (Shift (f,n))) implies (Im (Shift (f,n))) . x = (Shift ((Im f),n)) . x )
assume B1: x in dom (Im (Shift (f,n))) ; :: thesis: (Im (Shift (f,n))) . x = (Shift ((Im f),n)) . x
consider k being Nat such that
B2: ( k in dom f & x = k + n ) by B1, A0a, VALUED_1:39;
(Im (Shift (f,n))) . x = Im ((Shift (f,n)) . (k + n)) by B1, B2, COMSEQ_3:def 4
.= Im (f . k) by B2, VALUED_1:def 12
.= (Im f) . k by A0a, B2, COMSEQ_3:def 4
.= (Shift ((Im f),n)) . (k + n) by A0a, B2, VALUED_1:def 12 ;
hence (Im (Shift (f,n))) . x = (Shift ((Im f),n)) . x by B2; :: thesis: verum

end;

hence ( Re (Shift (f,n)) = Shift ((Re f),n) & Im (Shift (f,n)) = Shift ((Im f),n) ) by A1, A2, A3; :: thesis: verum