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;
A1: 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 B1: x in NAT ; :: thesis: (Shift (CastSeq seq,S),0 ) . x = (CastSeq seq,S) . x
reconsider x = x as Element of NAT by B1;
(Shift (CastSeq seq,S),0 ) . x = (CastSeq seq,S) . (x + 0 ) by DefShift01;
hence (Shift (CastSeq seq,S),0 ) . x = (CastSeq seq,S) . x ; :: thesis: verum

end;

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