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)

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