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 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) by Def41, NAT_1:def 3;
for m being Nat holds ((CastSeq ((Shift (seq,k)),S)) ^\ n) . m = ((CastSeq (seq,S)) ^\ (n + k)) . m

proof

let m be Nat; :: thesis: ((CastSeq ((Shift (seq,k)),S)) ^\ n) . m = ((CastSeq (seq,S)) ^\ (n + k)) . m
((CastSeq ((Shift (seq,k)),S)) ^\ n) . m = (CastSeq ((Shift (seq,k)),S)) . (m + n) by NAT_1:def 3
.= (CastSeq (seq,S)) . ((m + n) + k) by A1
.= (CastSeq (seq,S)) . (m + (n + k)) ;
hence ((CastSeq ((Shift (seq,k)),S)) ^\ n) . m = ((CastSeq (seq,S)) ^\ (n + k)) . m by NAT_1:def 3; :: thesis: verum

end;

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