dom f misses dom (Shift (seq,(len f))) by AFINSQ_1:72;
then reconsider g = f \/ (Shift (seq,(len f))) as Function by PARTFUN1:51, PARTFUN1:56;
reconsider g = g as NAT -defined COMPLEX -valued Function ;
A2: dom (f \/ (Shift (seq,(len f)))) = (dom f) \/ (dom (Shift (seq,(len f)))) by XTUPLE_0:23;
for x being object holds
( x in dom g iff x in NAT )

proof

let x be object ; :: thesis: ( x in dom g iff x in NAT )
( x in NAT implies x in dom g )

proof

assume x in NAT ; :: thesis: x in dom g
then reconsider x = x as Nat ;

per cases ( x < len f or x >= len f ) ;

suppose x < len f ; :: thesis: x in dom g

then x in Segm (len f) by NAT_1:44;
hence x in dom g by A2, XBOOLE_0:def 3; :: thesis: verum

end;

suppose x >= len f ; :: thesis: x in dom g

then consider k being Nat such that
B1: x = (len f) + k by NAT_1:10;
k in NAT by ORDINAL1:def 12;
then k in dom seq by COMSEQ_1:1;
then (len f) + k in dom (Shift (seq,(len f))) by VALUED_1:24;
hence x in dom g by A2, B1, XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

hence ( x in dom g iff x in NAT ) ; :: thesis: verum

end;

then A3: dom g = NAT by TARSKI:2;
for n being set st n in dom g holds
g . n is Element of COMPLEX by XCMPLX_0:def 2;
hence f \/ (Shift (seq,(len f))) is Complex_Sequence by A3, COMSEQ_1:1; :: thesis: verum