let S be non empty set ; :: thesis: for seq being Element of Inf_seq S holds Shift (seq,0) = seq
let seq be Element of Inf_seq S; :: thesis: Shift (seq,0) = seq
set cseq = CastSeq (seq,S);
for x being object st x in NAT holds
((CastSeq (seq,S)) ^\ 0) . x = (CastSeq (seq,S)) . x

proof

let x be object ; :: thesis: ( x in NAT implies ((CastSeq (seq,S)) ^\ 0) . x = (CastSeq (seq,S)) . x )
assume x in NAT ; :: thesis: ((CastSeq (seq,S)) ^\ 0) . x = (CastSeq (seq,S)) . x
then reconsider x = x as Element of NAT ;
((CastSeq (seq,S)) ^\ 0) . x = (CastSeq (seq,S)) . (x + 0) by NAT_1:def 3;
hence ((CastSeq (seq,S)) ^\ 0) . x = (CastSeq (seq,S)) . x ; :: thesis: verum

end;

then Shift (seq,0) = CastSeq (CastSeq (seq,S)) by FUNCT_2:12;
hence Shift (seq,0) = seq by Def41; :: thesis: verum