let f be complex-valued XFinSequence; :: thesis: for x being Nat holds (f ^ (seq_const 0)) . x = f . x
let x be Nat; :: thesis: (f ^ (seq_const 0)) . x = f . x
NAT = dom (f ^ (seq_const 0)) by COMSEQ_1:1
.= dom (f \/ (Shift ((seq_const 0),(dom f)))) ;
then (dom f) \/ (dom (Shift ((seq_const 0),(dom f)))) = NAT by XTUPLE_0:23;
then A1: x in (dom f) \/ (dom (Shift ((seq_const 0),(dom f)))) by ORDINAL1:def 12;
A1a: (Shift ((seq_const 0),(len f))) \/ (f ^ (seq_const 0)) = f ^ (seq_const 0) by XBOOLE_1:6;
(dom (Shift ((seq_const 0),(len f)))) /\ ((dom f) \/ (dom (Shift ((seq_const 0),(len f))))) = dom (Shift ((seq_const 0),(len f))) by XBOOLE_1:21;
then A2: (dom (Shift ((seq_const 0),(len f)))) /\ (dom (f ^ (seq_const 0))) = dom (Shift ((seq_const 0),(len f))) by XTUPLE_0:23;

per cases ( x in dom f or not x in dom f ) ;

suppose x in dom f ; :: thesis: (f ^ (seq_const 0)) . x = f . x

then (f ^ (seq_const 0)) . x = ((f ^ (seq_const 0)) | (len f)) . x by FUNCT_1:49
.= f . x ;
hence (f ^ (seq_const 0)) . x = f . x ; :: thesis: verum

end;

suppose B1: not x in dom f ; :: thesis: (f ^ (seq_const 0)) . x = f . x

then B2: x in dom (Shift ((seq_const 0),(dom f))) by A1, XBOOLE_0:def 3;
f . x = (seq_const 0) . ((len f) - x) by B1, FUNCT_1:def 2
.= (Shift ((seq_const 0),(len f))) . x
.= (f ^ (seq_const 0)) . x by A1a, A2, B2, PARTFUN1:2 ;
hence (f ^ (seq_const 0)) . x = f . x ; :: thesis: verum

end;

end;