let X be non empty set ; :: thesis: for s being sequence of X holds
( Shift ((s | (Segm 0)),1) = {} & Shift ((s | (Segm 1)),1) = <*(s . 0)*> & Shift ((s | (Segm 2)),1) = <*(s . 0),(s . 1)*> & ( for n being Nat holds Shift ((s | (Segm (n + 1))),1) = (Shift ((s | (Segm n)),1)) ^ <*(s . n)*> ) )
let s be sequence of X; :: thesis: ( Shift ((s | (Segm 0)),1) = {} & Shift ((s | (Segm 1)),1) = <*(s . 0)*> & Shift ((s | (Segm 2)),1) = <*(s . 0),(s . 1)*> & ( for n being Nat holds Shift ((s | (Segm (n + 1))),1) = (Shift ((s | (Segm n)),1)) ^ <*(s . n)*> ) )
thus Shift ((s | (Segm 0)),1) = {} ; :: thesis: ( Shift ((s | (Segm 1)),1) = <*(s . 0)*> & Shift ((s | (Segm 2)),1) = <*(s . 0),(s . 1)*> & ( for n being Nat holds Shift ((s | (Segm (n + 1))),1) = (Shift ((s | (Segm n)),1)) ^ <*(s . n)*> ) )
A1: dom (Shift ((s | (Segm 1)),1)) = Seg 1 by SH1;
then 1 in dom (Shift ((s | (Segm 1)),1)) by FINSEQ_1:2, TARSKI:def 1;
then ex n being Nat st
( n in dom (s | (Segm 1)) & 1 = n + 1 ) by VALUED_1:39;
then A3: (Shift ((s | (Segm 1)),1)) . 1 = (s | (Segm 1)) . 0 by VALUED_1:def 12;
0 in {0} by TARSKI:def 1;
then 0 in Segm 1 by CARD_1:49, ORDINAL1:def 17;
hence Shift ((s | (Segm 1)),1) = <*(s . 0)*> by A1, A3, FUNCT_1:49, FINSEQ_1:def 8; :: thesis: ( Shift ((s | (Segm 2)),1) = <*(s . 0),(s . 1)*> & ( for n being Nat holds Shift ((s | (Segm (n + 1))),1) = (Shift ((s | (Segm n)),1)) ^ <*(s . n)*> ) )
A6: dom (Shift ((s | (Segm 2)),1)) = Seg 2 by SH1;
then A4: len (Shift ((s | (Segm 2)),1)) = 2 by FINSEQ_1:def 3;
A5: Segm 2 = {0,1} by CARD_1:50, ORDINAL1:def 17;
A7: ( 1 in dom (Shift ((s | (Segm 2)),1)) & 2 in dom (Shift ((s | (Segm 2)),1)) ) by A6, FINSEQ_1:2, TARSKI:def 2;
then ex n being Nat st
( n in dom (s | (Segm 2)) & 1 = n + 1 ) by VALUED_1:39;
then A9: (Shift ((s | (Segm 2)),1)) . 1 = (s | (Segm 2)) . 0 by VALUED_1:def 12;
0 in Segm 2 by A5, TARSKI:def 2;
then A10: (Shift ((s | (Segm 2)),1)) . 1 = s . 0 by A9, FUNCT_1:49;
ex m being Nat st
( m in dom (s | (Segm 2)) & 2 = m + 1 ) by A7, VALUED_1:39;
then A12: (Shift ((s | (Segm 2)),1)) . 2 = (s | (Segm 2)) . 1 by VALUED_1:def 12;
1 in Segm 2 by A5, TARSKI:def 2;
hence Shift ((s | (Segm 2)),1) = <*(s . 0),(s . 1)*> by A4, A10, A12, FUNCT_1:49, FINSEQ_1:44; :: thesis: for n being Nat holds Shift ((s | (Segm (n + 1))),1) = (Shift ((s | (Segm n)),1)) ^ <*(s . n)*>
hereby :: thesis: verum
let n be Nat; :: thesis: Shift ((s | (Segm (n + 1))),1) = (Shift ((s | (Segm n)),1)) ^ <*(s . n)*>
X3: n is Element of NAT by ORDINAL1:def 12;
( dom (Shift ((s | (Segm (n + 1))),1)) = Seg (n + 1) & dom (Shift ((s | (Segm n)),1)) = Seg n ) by SH1;
then A13: ( len (Shift ((s | (Segm (n + 1))),1)) = n + 1 & len (Shift ((s | (Segm n)),1)) = n ) by X3, FINSEQ_1:def 3;
A14: len <*(s . n)*> = 1 by FINSEQ_1:40;
A15: for k being Nat st k in dom (Shift ((s | (Segm n)),1)) holds
(Shift ((s | (Segm (n + 1))),1)) . k = (Shift ((s | (Segm n)),1)) . k
proof
let k be Nat; :: thesis: ( k in dom (Shift ((s | (Segm n)),1)) implies (Shift ((s | (Segm (n + 1))),1)) . k = (Shift ((s | (Segm n)),1)) . k )
assume A17: k in dom (Shift ((s | (Segm n)),1)) ; :: thesis: (Shift ((s | (Segm (n + 1))),1)) . k = (Shift ((s | (Segm n)),1)) . k
then A18: k in Seg n by SH1;
then 1 <= k by FINSEQ_1:1;
then reconsider k1 = k - 1 as Element of NAT by NAT_1:21;
Seg n c= Seg (n + 1) by FINSEQ_3:18;
then k in Seg (n + 1) by A18;
then A19: k in dom (Shift ((s | (Segm (n + 1))),1)) by SH1;
k = k1 + 1 ;
then ( (Shift ((s | (Segm n)),1)) . k = s . k1 & (Shift ((s | (Segm (n + 1))),1)) . k = s . k1 ) by A17, A19, SH3;
hence (Shift ((s | (Segm (n + 1))),1)) . k = (Shift ((s | (Segm n)),1)) . k ; :: thesis: verum
end;
for k being Nat st k in dom <*(s . n)*> holds
(Shift ((s | (Segm (n + 1))),1)) . ((len (Shift ((s | (Segm n)),1))) + k) = <*(s . n)*> . k
proof
let k be Nat; :: thesis: ( k in dom <*(s . n)*> implies (Shift ((s | (Segm (n + 1))),1)) . ((len (Shift ((s | (Segm n)),1))) + k) = <*(s . n)*> . k )
assume k in dom <*(s . n)*> ; :: thesis: (Shift ((s | (Segm (n + 1))),1)) . ((len (Shift ((s | (Segm n)),1))) + k) = <*(s . n)*> . k
then k in Seg 1 by FINSEQ_1:def 8;
then A20: k = 1 by FINSEQ_1:2, TARSKI:def 1;
then A23: <*(s . n)*> . k = s . n by FINSEQ_1:def 8;
A21: n is Element of NAT by ORDINAL1:def 12;
dom (Shift ((s | (Segm n)),1)) = Seg n by SH1;
then A22: len (Shift ((s | (Segm n)),1)) = n by A21, FINSEQ_1:def 3;
n + 1 in Seg (n + 1) by FINSEQ_1:4;
then n + 1 in dom (Shift ((s | (Segm (n + 1))),1)) by SH1;
hence (Shift ((s | (Segm (n + 1))),1)) . ((len (Shift ((s | (Segm n)),1))) + k) = <*(s . n)*> . k by A23, A22, A20, SH3; :: thesis: verum
end;
hence Shift ((s | (Segm (n + 1))),1) = (Shift ((s | (Segm n)),1)) ^ <*(s . n)*> by A13, A14, A15, FINSEQ_3:38; :: thesis: verum
end;