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: dom (N Shift (idseq m)) = { (k + N) where k is Nat : k in dom (idseq m) } by VALUED_1:def 12;
A4: (Seg (n + m)) \ (Seg n) c= dom (N Shift (idseq m))

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (Seg (n + m)) \ (Seg n) or x in dom (N Shift (idseq m)) )
assume A5: x in (Seg (n + m)) \ (Seg n) ; :: thesis: x in dom (N Shift (idseq m))
reconsider i = x as Element of NAT by A5;
A6: i in Seg (n + m) by A5, XBOOLE_0:def 5;
not i in Seg n by A5, XBOOLE_0:def 5;
then A7: ( i < 1 or i > n ) ;
then reconsider IN = i - n as Element of NAT by A6, FINSEQ_1:1, NAT_1:21;
A8: n + IN = i ;
i <= n + m by A6, FINSEQ_1:1;
then A9: IN <= m by A8, XREAL_1:8;
IN >= 1 by A6, A7, A8, FINSEQ_1:1, NAT_1:19;
then IN in dom (idseq m) by A9;
then n + IN in dom (N Shift (idseq m)) by A3;
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 object ; :: 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 Nat such that
A10: k + n = x and
A11: k in dom (idseq m) by A3;
k <= m by A11, FINSEQ_1:1;
then A12: n + k <= n + m by XREAL_1:7;
1 <= k by A11, FINSEQ_1:1;
then A13: n + 1 <= n + k by XREAL_1:7;
then n + k > n by NAT_1:13;
then A14: not k + n in Seg n by FINSEQ_1:1;
1 <= n + 1 by NAT_1:11;
then 1 <= n + k by A13, XXREAL_0:2;
then n + k in Seg (n + m) by A12;
hence x in (Seg (n + m)) \ (Seg n) by A10, A14, XBOOLE_0:def 5; :: thesis: verum

end;

then (Seg (n + m)) \ (Seg n) = dom (N Shift (idseq m)) by A4;
hence (Sgm ((Seg (n + m)) \ (Seg n))) . i = n + i by A1, A2, VALUED_1:44; :: thesis: verum