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 set st x in NAT holds
(Shift ((CastSeq (seq,S)),0)) . x = (CastSeq (seq,S)) . x

proof

let x be set ; :: thesis: ( x in NAT implies (Shift ((CastSeq (seq,S)),0)) . x = (CastSeq (seq,S)) . x )
assume x in NAT ; :: thesis: (Shift ((CastSeq (seq,S)),0)) . x = (CastSeq (seq,S)) . x
then reconsider x = x as Element of NAT ;
(Shift ((CastSeq (seq,S)),0)) . x = (CastSeq (seq,S)) . (x + 0) by Def43;
hence (Shift ((CastSeq (seq,S)),0)) . x = (CastSeq (seq,S)) . x ; :: thesis: verum

end;

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