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 () = Seg (len ()) by FINSEQ_1:def 3;
A3: dom (N Shift ()) = { (k + N) where k is Nat : k in dom () } by VALUED_1:def 12;
A4: (Seg (n + m)) \ (Seg n) c= dom (N Shift ())
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 ()) )
assume A5: x in (Seg (n + m)) \ (Seg n) ; :: thesis: x in dom (N Shift ())
reconsider i = x as Element of NAT by A5;
A6: i in Seg (n + m) by ;
not i in Seg n by ;
then A7: ( i < 1 or i > n ) ;
then reconsider IN = i - n as Element of NAT by ;
A8: n + IN = i ;
i <= n + m by ;
then A9: IN <= m by ;
IN >= 1 by ;
then IN in dom () by A9;
then n + IN in dom (N Shift ()) by A3;
hence x in dom (N Shift ()) ; :: thesis: verum
end;
dom (N Shift ()) c= (Seg (n + m)) \ (Seg n)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom (N Shift ()) or x in (Seg (n + m)) \ (Seg n) )
assume x in dom (N Shift ()) ; :: thesis: x in (Seg (n + m)) \ (Seg n)
then consider k being Nat such that
A10: k + n = x and
A11: k in dom () by A3;
k <= m by ;
then A12: n + k <= n + m by XREAL_1:7;
1 <= k by ;
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 ;
then n + k in Seg (n + m) by A12;
hence x in (Seg (n + m)) \ (Seg n) by ; :: thesis: verum
end;
then (Seg (n + m)) \ (Seg n) = dom (N Shift ()) by A4;
hence (Sgm ((Seg (n + m)) \ (Seg n))) . i = n + i by ; :: thesis: verum