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;
A1: 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 Def42;
hence (CastSeq (Shift seq,k),S) . m = (CastSeq seq,S) . (m + k) by Def43; :: thesis: verum

end;

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 Def43
.= (CastSeq seq,S) . ((m + n) + k) by A1
.= (CastSeq seq,S) . (m + (n + k)) ;
hence (Shift (CastSeq (Shift seq,k),S),n) . m = (Shift (CastSeq seq,S),(n + k)) . m by Def43; :: thesis: verum

end;

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