let X be non empty set ; :: thesis:
let s be sequence of X; :: thesis:
let n be Nat; :: thesis:
Segm n c= NAT ;
then NAT /\ (Segm n) = Segm n by XBOOLE_1:28;
then (dom s) /\ (Segm n) = Segm n by FUNCT_2:def 1;
then A2: dom (s | (Segm n)) = Segm n by RELAT_1:61;
A3: dom (Shift ((s | (Segm n)),1)) = { (m + 1) where m is Nat : m in dom (s | (Segm n)) } by VALUED_1:def 12;

let k be object ; :: thesis:
assume k in dom (Shift ((s | (Segm n)),1)) ; :: thesis:
then consider m being Nat such that
A4: ( k = m + 1 & m in dom (s | (Segm n)) ) by A3;

end;

then reconsider n1 = n - 1 as Element of NAT by NAT_1:20;
reconsider n1 = n1 as Nat ;
B3: n = n1 + 1 ;
m in Segm (n1 + 1) by A4, RELAT_1:57;
then m in succ (Segm n1) by NAT_1:38;
then m in { l where l is Nat : l <= n1 } by NAT_1:54;
then consider l being Nat such that
A5: ( m = l & l <= n1 ) ;
( 1 <= m + 1 & m + 1 <= n ) by A5, B3, NAT_1:11, XREAL_1:6;
hence k in Seg n by A4, FINSEQ_1:1; :: thesis:

end;

let k be object ; :: thesis:
assume k in Seg n ; :: thesis:
then k in { l where l is Nat : ( 1 <= l & l <= n ) } by FINSEQ_1:def 1;
then consider l being Nat such that
A7: ( k = l & 1 <= l & l <= n ) ;
0 < l by A7;
then reconsider l1 = l - 1 as Element of NAT by NAT_1:20;
0 < n by A7;
then reconsider i = n - 1 as Element of NAT by NAT_1:20;
B5: n = i + 1 ;
B9: k = l1 + 1 by A7;
l1 <= i by A7, XREAL_1:9;
then l1 in { m where m is Nat : m <= i } ;
then l1 in succ (Segm i) by NAT_1:54;
then l1 in Segm n by B5, NAT_1:38;
hence k in dom (Shift ((s | (Segm n)),1)) by A2, A3, B9; :: thesis:

end;