let i, m, n be Nat; :: thesis: ( i in Seg m implies (Sgm ((Seg (n + m)) \ (Seg n))) . i = n + i )
assume A1: i in Seg m ; :: thesis: (Sgm ((Seg (n + m)) \ (Seg n))) . i = n + i
reconsider N = n as Element of NAT by ORDINAL1:def 12;
set I = idseq m;
A2: dom (idseq m) = Seg (len (idseq m)) by FINSEQ_1:def 3;
A3: len (idseq m) = m by CARD_1:def 7;
A4: dom (N Shift (idseq m)) = { (N + k) where k is Element of NAT : k in dom (idseq m) } by PNPROC_1:def 14;
A5: (Seg (n + m)) \ (Seg n) c= dom (N Shift (idseq m))

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (Seg (n + m)) \ (Seg n) or x in dom (N Shift (idseq m)) )
assume A6: x in (Seg (n + m)) \ (Seg n) ; :: thesis: x in dom (N Shift (idseq m))
reconsider i = x as Element of NAT by A6;
A7: i in Seg (n + m) by A6, XBOOLE_0:def 5;
not i in Seg n by A6, XBOOLE_0:def 5;
then A8: ( i < 1 or i > n ) ;
then reconsider IN = i - n as Element of NAT by A7, FINSEQ_1:1, NAT_1:21;
A9: n + IN = i ;
i <= n + m by A7, FINSEQ_1:1;
then A10: IN <= m by A9, XREAL_1:8;
IN >= 1 by A7, A8, A9, FINSEQ_1:1, NAT_1:19;
then IN in dom (idseq m) by A2, A3, A10;
then n + IN in dom (N Shift (idseq m)) by A4;
hence x in dom (N Shift (idseq m)) ; :: thesis: verum

end;

dom (N Shift (idseq m)) c= (Seg (n + m)) \ (Seg n)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in dom (N Shift (idseq m)) or x in (Seg (n + m)) \ (Seg n) )
assume x in dom (N Shift (idseq m)) ; :: thesis: x in (Seg (n + m)) \ (Seg n)
then consider k being Element of NAT such that
A11: n + k = x and
A12: k in dom (idseq m) by A4;
k <= m by A2, A3, A12, FINSEQ_1:1;
then A13: n + k <= n + m by XREAL_1:7;
1 <= k by A2, A12, FINSEQ_1:1;
then A14: n + 1 <= n + k by XREAL_1:7;
then n + k > n by NAT_1:13;
then A15: not k + n in Seg n by FINSEQ_1:1;
1 <= n + 1 by NAT_1:11;
then 1 <= n + k by A14, XXREAL_0:2;
then n + k in Seg (n + m) by A13;
hence x in (Seg (n + m)) \ (Seg n) by A11, A15, XBOOLE_0:def 5; :: thesis: verum

end;

then (Seg (n + m)) \ (Seg n) = dom (N Shift (idseq m)) by A5, XBOOLE_0:def 10;
hence (Sgm ((Seg (n + m)) \ (Seg n))) . i = n + i by A1, A2, A3, PNPROC_1:56; :: thesis: verum