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))

hence (Sgm ((Seg (n + m)) \ (Seg n))) . i = n + i by A1, A2, VALUED_1:44; :: thesis: verum

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

dom (N Shift (idseq m)) c= (Seg (n + m)) \ (Seg n)
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;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

proof

then
(Seg (n + m)) \ (Seg n) = dom (N Shift (idseq m))
by A4;
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;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

hence (Sgm ((Seg (n + m)) \ (Seg n))) . i = n + i by A1, A2, VALUED_1:44; :: thesis: verum