defpred S₁[ Nat] means for n, k, i being Nat st n = $1 + 1 & k in Seg n & i in Seg $1 holds
( ( 1 <= i & i < k implies (Sgm ((Seg n) \ {k})) . i = i ) & ( k <= i & i <= $1 implies (Sgm ((Seg n) \ {k})) . i = i + 1 ) );
let i, k, m, n be Nat; :: thesis: ( n = m + 1 & k in Seg n & i in Seg m implies ( ( 1 <= i & i < k implies (Sgm ((Seg n) \ {k})) . i = i ) & ( k <= i & i <= m implies (Sgm ((Seg n) \ {k})) . i = i + 1 ) ) )
assume that
A1: n = m + 1 and
A2: k in Seg n and
A3: i in Seg m ; :: thesis: ( ( 1 <= i & i < k implies (Sgm ((Seg n) \ {k})) . i = i ) & ( k <= i & i <= m implies (Sgm ((Seg n) \ {k})) . i = i + 1 ) )
A4: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A5: S₁[k] ; :: thesis: S₁[k + 1]
let g, i, n be Nat; :: thesis: ( g = (k + 1) + 1 & i in Seg g & n in Seg (k + 1) implies ( ( 1 <= n & n < i implies (Sgm ((Seg g) \ {i})) . n = n ) & ( i <= n & n <= k + 1 implies (Sgm ((Seg g) \ {i})) . n = n + 1 ) ) )
assume that
A6: g = (k + 1) + 1 and
A7: i in Seg g and
A8: n in Seg (k + 1) ; :: thesis: ( ( 1 <= n & n < i implies (Sgm ((Seg g) \ {i})) . n = n ) & ( i <= n & n <= k + 1 implies (Sgm ((Seg g) \ {i})) . n = n + 1 ) )
A9: 1 <= i by A7, FINSEQ_1:1;
set X = (Seg g) \ {i};
A10: len (Sgm ((Seg g) \ {i})) = k + 1 by A6, A7, Th116;
A11: 1 <= n by A8, FINSEQ_1:1;
A12: i <= g by A7, FINSEQ_1:1;
A13: (Seg g) \ {i} c= Seg g by XBOOLE_1:36;
then A14: rng (Sgm ((Seg g) \ {i})) = (Seg g) \ {i} by FINSEQ_1:def 13;
A15: n <= k + 1 by A8, FINSEQ_1:1;

now

per cases ( i = g or i <> g ) ;

suppose A16: i = g ; :: thesis: ( ( 1 <= n & n < i implies (Sgm ((Seg g) \ {i})) . n = n ) & ( i <= n & n <= k + 1 implies (Sgm ((Seg g) \ {i})) . n = n + 1 ) )

then A17: k + 1 < i by A6, NAT_1:13;
(Seg g) \ {i} = Seg (k + 1)

proof

thus (Seg g) \ {i} c= Seg (k + 1) :: according to XBOOLE_0:def 10 :: thesis: Seg (k + 1) c= (Seg g) \ {i}

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (Seg g) \ {i} or x in Seg (k + 1) )
A18: Seg g = { J where J is Element of NAT : ( 1 <= J & J <= g ) } by FINSEQ_1:def 1;
assume A19: x in (Seg g) \ {i} ; :: thesis: x in Seg (k + 1)
then x in Seg g by XBOOLE_0:def 5;
then consider J being Element of NAT such that
A20: x = J and
A21: 1 <= J and
A22: J <= g by A18;
not x in {i} by A19, XBOOLE_0:def 5;
then x <> i by TARSKI:def 1;
then J < g by A16, A20, A22, XXREAL_0:1;
then J <= k + 1 by A6, NAT_1:13;
hence x in Seg (k + 1) by A20, A21, FINSEQ_1:1; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Seg (k + 1) or x in (Seg g) \ {i} )
assume x in Seg (k + 1) ; :: thesis: x in (Seg g) \ {i}
then x in { J where J is Element of NAT : ( 1 <= J & J <= k + 1 ) } by FINSEQ_1:def 1;
then consider J being Element of NAT such that
A23: x = J and
A24: 1 <= J and
A25: J <= k + 1 ;
k + 1 <= g by A6, NAT_1:11;
then J <= g by A25, XXREAL_0:2;
then A26: J in Seg g by A24, FINSEQ_1:1;
not J in {i} by A17, A25, TARSKI:def 1;
hence x in (Seg g) \ {i} by A23, A26, XBOOLE_0:def 5; :: thesis: verum

end;

then Sgm ((Seg g) \ {i}) = idseq (k + 1) by Th54;
hence ( 1 <= n & n < i implies (Sgm ((Seg g) \ {i})) . n = n ) by A8, FUNCT_1:17; :: thesis: ( i <= n & n <= k + 1 implies (Sgm ((Seg g) \ {i})) . n = n + 1 )
thus ( i <= n & n <= k + 1 implies (Sgm ((Seg g) \ {i})) . n = n + 1 ) by A6, A16, NAT_1:13; :: thesis: verum

end;

suppose A27: i <> g ; :: thesis: ( ( 1 <= n & n < i implies (Sgm ((Seg g) \ {i})) . n = n ) & ( i <= n & n <= k + 1 implies (Sgm ((Seg g) \ {i})) . n = n + 1 ) )

set A = { l where l is Element of NAT : ( 1 <= l & l <= g & l <> i ) } ;
A28: (Seg g) \ {i} = { l where l is Element of NAT : ( 1 <= l & l <= g & l <> i ) }

proof

thus (Seg g) \ {i} c= { l where l is Element of NAT : ( 1 <= l & l <= g & l <> i ) } :: according to XBOOLE_0:def 10 :: thesis: { l where l is Element of NAT : ( 1 <= l & l <= g & l <> i ) } c= (Seg g) \ {i}

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (Seg g) \ {i} or x in { l where l is Element of NAT : ( 1 <= l & l <= g & l <> i ) } )
A29: Seg g = { J where J is Element of NAT : ( 1 <= J & J <= g ) } by FINSEQ_1:def 1;
assume A30: x in (Seg g) \ {i} ; :: thesis: x in { l where l is Element of NAT : ( 1 <= l & l <= g & l <> i ) }
then x in Seg g by XBOOLE_0:def 5;
then consider m being Element of NAT such that
A31: x = m and
A32: 1 <= m and
A33: m <= g by A29;
not x in {i} by A30, XBOOLE_0:def 5;
then m <> i by A31, TARSKI:def 1;
hence x in { l where l is Element of NAT : ( 1 <= l & l <= g & l <> i ) } by A31, A32, A33; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { l where l is Element of NAT : ( 1 <= l & l <= g & l <> i ) } or x in (Seg g) \ {i} )
assume x in { l where l is Element of NAT : ( 1 <= l & l <= g & l <> i ) } ; :: thesis: x in (Seg g) \ {i}
then consider m being Element of NAT such that
A34: x = m and
A35: 1 <= m and
A36: m <= g and
A37: m <> i ;
A38: not m in {i} by A37, TARSKI:def 1;
m in Seg g by A35, A36, FINSEQ_1:1;
hence x in (Seg g) \ {i} by A34, A38, XBOOLE_0:def 5; :: thesis: verum

end;

1 <= k + 1 by A11, A15, XXREAL_0:2;
then k + 1 in dom (Sgm ((Seg g) \ {i})) by A10, Th27;
then (Sgm ((Seg g) \ {i})) . (k + 1) in (Seg g) \ {i} by A14, FUNCT_1:def 3;
then A39: ex J being Element of NAT st
( (Sgm ((Seg g) \ {i})) . (k + 1) = J & 1 <= J & J <= g & J <> i ) by A28;
A40: g in NAT by ORDINAL1:def 12;
1 <= g by A9, A12, XXREAL_0:2;
then g in rng (Sgm ((Seg g) \ {i})) by A14, A27, A28, A40;
then consider x being Nat such that
A41: x in dom (Sgm ((Seg g) \ {i})) and
A42: (Sgm ((Seg g) \ {i})) . x = g by FINSEQ_2:10;
1 <= x by A41, Th27;
then A43: k + 1 <= x by A13, A10, A39, A42, FINSEQ_1:def 13;
A44: i < g by A12, A27, XXREAL_0:1;
then A45: i <= k + 1 by A6, NAT_1:13;
A46: x <= k + 1 by A10, A41, Th27;

now

per cases ( n = k + 1 or n < k + 1 ) by A15, XXREAL_0:1;

suppose A47: n = k + 1 ; :: thesis: ( ( 1 <= n & n < i implies (Sgm ((Seg g) \ {i})) . n = n ) & ( i <= n & n <= k + 1 implies (Sgm ((Seg g) \ {i})) . n = n + 1 ) )

hence ( 1 <= n & n < i implies (Sgm ((Seg g) \ {i})) . n = n ) by A6, A44, NAT_1:13; :: thesis: ( i <= n & n <= k + 1 implies (Sgm ((Seg g) \ {i})) . n = n + 1 )
thus ( i <= n & n <= k + 1 implies (Sgm ((Seg g) \ {i})) . n = n + 1 ) by A6, A42, A46, A43, A47, XXREAL_0:1; :: thesis: verum

end;

suppose A48: n < k + 1 ; :: thesis: ( ( 1 <= n & n < i implies (Sgm ((Seg g) \ {i})) . n = n ) & ( i <= n & n <= k + 1 implies (Sgm ((Seg g) \ {i})) . n = n + 1 ) )

set Y = (Seg (k + 1)) \ {i};

A49: now

let j1, j be Element of NAT ; :: thesis: ( j1 in (Seg (k + 1)) \ {i} & j in {g} implies j1 < j )
assume that
A50: j1 in (Seg (k + 1)) \ {i} and
A51: j in {g} ; :: thesis: j1 < j
j1 in Seg (k + 1) by A50, XBOOLE_0:def 5;
then A52: j1 <= k + 1 by FINSEQ_1:1;
j = g by A51, TARSKI:def 1;
hence j1 < j by A6, A52, NAT_1:13; :: thesis: verum

end;

A53: (Seg g) \ {i} = ((Seg (k + 1)) \ {i}) \/ {g}

proof

thus (Seg g) \ {i} c= ((Seg (k + 1)) \ {i}) \/ {g} :: according to XBOOLE_0:def 10 :: thesis: ((Seg (k + 1)) \ {i}) \/ {g} c= (Seg g) \ {i}

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (Seg g) \ {i} or x in ((Seg (k + 1)) \ {i}) \/ {g} )
assume x in (Seg g) \ {i} ; :: thesis: x in ((Seg (k + 1)) \ {i}) \/ {g}
then consider J being Element of NAT such that
A54: x = J and
A55: 1 <= J and
A56: J <= g and
A57: J <> i by A28;

now

per cases ( J = g or J < g ) by A56, XXREAL_0:1;

suppose J = g ; :: thesis: x in ((Seg (k + 1)) \ {i}) \/ {g}

then x in {g} by A54, TARSKI:def 1;
hence x in ((Seg (k + 1)) \ {i}) \/ {g} by XBOOLE_0:def 3; :: thesis: verum

end;

suppose J < g ; :: thesis: x in ((Seg (k + 1)) \ {i}) \/ {g}

then J <= k + 1 by A6, NAT_1:13;
then A58: J in Seg (k + 1) by A55, FINSEQ_1:1;
not J in {i} by A57, TARSKI:def 1;
then x in (Seg (k + 1)) \ {i} by A54, A58, XBOOLE_0:def 5;
hence x in ((Seg (k + 1)) \ {i}) \/ {g} by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

hence x in ((Seg (k + 1)) \ {i}) \/ {g} ; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in ((Seg (k + 1)) \ {i}) \/ {g} or x in (Seg g) \ {i} )
assume A59: x in ((Seg (k + 1)) \ {i}) \/ {g} ; :: thesis: x in (Seg g) \ {i}

now

per cases ( x in (Seg (k + 1)) \ {i} or x in {g} ) by A59, XBOOLE_0:def 3;

suppose A60: x in (Seg (k + 1)) \ {i} ; :: thesis: x in (Seg g) \ {i}

A61: Seg (k + 1) = { s where s is Element of NAT : ( 1 <= s & s <= k + 1 ) } by FINSEQ_1:def 1;
x in Seg (k + 1) by A60, XBOOLE_0:def 5;
then consider s being Element of NAT such that
A62: x = s and
A63: 1 <= s and
A64: s <= k + 1 by A61;
not x in {i} by A60, XBOOLE_0:def 5;
then A65: s <> i by A62, TARSKI:def 1;
k + 1 <= g by A6, NAT_1:11;
then s <= g by A64, XXREAL_0:2;
hence x in (Seg g) \ {i} by A28, A62, A63, A65; :: thesis: verum

end;

suppose x in {g} ; :: thesis: x in (Seg g) \ {i}

then A66: x = g by TARSKI:def 1;
1 <= g by A9, A12, XXREAL_0:2;
hence x in (Seg g) \ {i} by A27, A28, A66, A40; :: thesis: verum

end;

end;

end;

hence x in (Seg g) \ {i} ; :: thesis: verum

end;

then {g} c= (Seg g) \ {i} by XBOOLE_1:7;
then A67: {g} c= Seg g by A13, XBOOLE_1:1;
(Seg (k + 1)) \ {i} c= (Seg g) \ {i} by A53, XBOOLE_1:7;
then (Seg (k + 1)) \ {i} c= Seg g by A13, XBOOLE_1:1;
then A68: Sgm ((Seg g) \ {i}) = (Sgm ((Seg (k + 1)) \ {i})) ^ (Sgm {g}) by A53, A49, A67, Th48;
n <= k by A48, NAT_1:13;
then A69: n in Seg k by A11, FINSEQ_1:1;
A70: i in Seg (k + 1) by A9, A45, FINSEQ_1:1;
then len (Sgm ((Seg (k + 1)) \ {i})) = k by Th116;
then A71: n in dom (Sgm ((Seg (k + 1)) \ {i})) by A69, FINSEQ_1:def 3;
n <= k by A48, NAT_1:13;
then A72: n in Seg k by A11, FINSEQ_1:1;
then A73: ( 1 <= n & n < i implies (Sgm ((Seg (k + 1)) \ {i})) . n = n ) by A5, A70;

now

assume that
A74: 1 <= n and
A75: n < i ; :: thesis: (Sgm ((Seg g) \ {i})) . n = n
n in Seg (len (Sgm ((Seg (k + 1)) \ {i}))) by A72, A70, Th116;
then n in dom (Sgm ((Seg (k + 1)) \ {i})) by FINSEQ_1:def 3;
hence (Sgm ((Seg g) \ {i})) . n = n by A73, A68, A74, A75, FINSEQ_1:def 7; :: thesis: verum

end;

hence ( 1 <= n & n < i implies (Sgm ((Seg g) \ {i})) . n = n ) ; :: thesis: ( i <= n & n <= k + 1 implies (Sgm ((Seg g) \ {i})) . n = n + 1 )
assume that
A76: i <= n and
n <= k + 1 ; :: thesis: (Sgm ((Seg g) \ {i})) . n = n + 1
( i <= n & n <= k implies (Sgm ((Seg (k + 1)) \ {i})) . n = n + 1 ) by A5, A72, A70;
hence (Sgm ((Seg g) \ {i})) . n = n + 1 by A48, A68, A76, A71, FINSEQ_1:def 7, NAT_1:13; :: thesis: verum

end;

end;

end;

hence ( ( 1 <= n & n < i implies (Sgm ((Seg g) \ {i})) . n = n ) & ( i <= n & n <= k + 1 implies (Sgm ((Seg g) \ {i})) . n = n + 1 ) ) ; :: thesis: verum

end;

end;

end;

hence ( ( 1 <= n & n < i implies (Sgm ((Seg g) \ {i})) . n = n ) & ( i <= n & n <= k + 1 implies (Sgm ((Seg g) \ {i})) . n = n + 1 ) ) ; :: thesis: verum

end;

A77: S₁[ 0 ] ;
for k being Nat holds S₁[k] from NAT_1:sch 2(A77, A4);
hence ( ( 1 <= i & i < k implies (Sgm ((Seg n) \ {k})) . i = i ) & ( k <= i & i <= m implies (Sgm ((Seg n) \ {k})) . i = i + 1 ) ) by A1, A2, A3; :: thesis: verum