let X be non empty set ; :: thesis: for s being sequence of X
for n being Nat holds dom (Shift ((s | (Segm n)),1)) = Seg n
let s be sequence of X; :: thesis: for n being Nat holds dom (Shift ((s | (Segm n)),1)) = Seg n
let n be Nat; :: thesis: dom (Shift ((s | (Segm n)),1)) = Seg n
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;

now :: thesis: for k being object st k in dom (Shift ((s | (Segm n)),1)) holds
k in Seg n

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

per cases ( n = 0 or n <> 0 ) ;

suppose n = 0 ; :: thesis: b₁ in Seg n

hence k in Seg n by A4; :: thesis: verum

end;

suppose n <> 0 ; :: thesis: b₁ in Seg n

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: verum

end;

end;

end;

then A6: dom (Shift ((s | (Segm n)),1)) c= Seg n ;

now :: thesis: for k being object st k in Seg n holds
k in dom (Shift ((s | (Segm n)),1))

let k be object ; :: thesis: ( k in Seg n implies k in dom (Shift ((s | (Segm n)),1)) )
assume k in Seg n ; :: thesis: k in dom (Shift ((s | (Segm n)),1))
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: verum

end;

then Seg n c= dom (Shift ((s | (Segm n)),1)) ;
hence dom (Shift ((s | (Segm n)),1)) = Seg n by A6, XBOOLE_0:def 10; :: thesis: verum