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