let k, n be Nat; :: thesis: for S being non empty set
for seq being Element of Inf_seq S holds Shift (Shift seq,k),n = Shift seq,(n + k)
let S be non empty set ; :: thesis: for seq being Element of Inf_seq S holds Shift (Shift seq,k),n = Shift seq,(n + k)
let seq be Element of Inf_seq S; :: thesis: Shift (Shift seq,k),n = Shift seq,(n + k)
set nk = n + k;
set t1 = Shift seq,k;
set t2 = Shift (Shift seq,k),n;
set t3 = Shift seq,(n + k);
set cseq = CastSeq seq,S;
set ct1 = CastSeq (Shift seq,k),S;
A4: for m being Nat holds (CastSeq (Shift seq,k),S) . m = (CastSeq seq,S) . (m + k)

proof

let m be Nat; :: thesis: (CastSeq (Shift seq,k),S) . m = (CastSeq seq,S) . (m + k)
(CastSeq (Shift seq,k),S) . m = (Shift (CastSeq seq,S),k) . m by DefCasetSeq2;
hence (CastSeq (Shift seq,k),S) . m = (CastSeq seq,S) . (m + k) by DefShift01; :: thesis: verum

end;

A5: for m being Nat holds (Shift (CastSeq (Shift seq,k),S),n) . m = (Shift (CastSeq seq,S),(n + k)) . m

proof

let m be Nat; :: thesis: (Shift (CastSeq (Shift seq,k),S),n) . m = (Shift (CastSeq seq,S),(n + k)) . m
(Shift (CastSeq (Shift seq,k),S),n) . m = (CastSeq (Shift seq,k),S) . (m + n) by DefShift01
.= (CastSeq seq,S) . ((m + n) + k) by A4
.= (CastSeq seq,S) . (m + (n + k)) ;
hence (Shift (CastSeq (Shift seq,k),S),n) . m = (Shift (CastSeq seq,S),(n + k)) . m by DefShift01; :: thesis: verum

end;

for x being set st x in NAT holds
(Shift (CastSeq (Shift seq,k),S),n) . x = (Shift (CastSeq seq,S),(n + k)) . x by A5;
hence Shift (Shift seq,k),n = Shift seq,(n + k) by FUNCT_2:18; :: thesis: verum