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, Th105;
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;
A14: rng (Sgm ((Seg g) \ {i})) = (Seg g) \ {i} by FINSEQ_1:def 14;
A15: n <= k + 1 by A8, FINSEQ_1:1;

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

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 object ; :: 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 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 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 object ; :: 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 Nat : ( 1 <= J & J <= k + 1 ) } by FINSEQ_1:def 1;
then consider J being 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 Th46;
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 Nat : ( 1 <= l & l <= g & l <> i ) } ;
A28: (Seg g) \ {i} = { l where l is Nat : ( 1 <= l & l <= g & l <> i ) }

proof

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

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (Seg g) \ {i} or x in { l where l is Nat : ( 1 <= l & l <= g & l <> i ) } )
A29: Seg g = { J where J is Nat : ( 1 <= J & J <= g ) } by FINSEQ_1:def 1;
assume A30: x in (Seg g) \ {i} ; :: thesis: x in { l where l is Nat : ( 1 <= l & l <= g & l <> i ) }
then x in Seg g by XBOOLE_0:def 5;
then consider m being 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 Nat : ( 1 <= l & l <= g & l <> i ) } by A31, A32, A33; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { l where l is Nat : ( 1 <= l & l <= g & l <> i ) } or x in (Seg g) \ {i} )
assume x in { l where l is Nat : ( 1 <= l & l <= g & l <> i ) } ; :: thesis: x in (Seg g) \ {i}
then consider m being 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, Th25;
then (Sgm ((Seg g) \ {i})) . (k + 1) in (Seg g) \ {i} by A14, FUNCT_1:def 3;
then A39: ex J being Nat st
( (Sgm ((Seg g) \ {i})) . (k + 1) = J & 1 <= J & J <= g & J <> i ) by A28;
1 <= g by A9, A12, XXREAL_0:2;
then g in rng (Sgm ((Seg g) \ {i})) by A14, A27, A28;
then consider x being Nat such that
A40: x in dom (Sgm ((Seg g) \ {i})) and
A41: (Sgm ((Seg g) \ {i})) . x = g by FINSEQ_2:10;
1 <= x by A40, Th25;
then A42: k + 1 <= x by A10, A39, A41, FINSEQ_1:def 14;
A43: i < g by A12, A27, XXREAL_0:1;
then A44: i <= k + 1 by A6, NAT_1:13;
A45: x <= k + 1 by A10, A40, Th25;

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

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

suppose A46: 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, A43, 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, A41, A45, A42, A46, XXREAL_0:1; :: thesis: verum

end;

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

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

A48: now :: thesis: for j1, j being Nat st j1 in (Seg (k + 1)) \ {i} & j in {g} holds
j1 < j

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

end;

A52: (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 object ; :: 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 Nat such that
A53: x = J and
A54: 1 <= J and
A55: J <= g and
A56: J <> i by A28;

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

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

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

then x in {g} by A53, 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 A57: J in Seg (k + 1) by A54, FINSEQ_1:1;
not J in {i} by A56, TARSKI:def 1;
then x in (Seg (k + 1)) \ {i} by A53, A57, 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 object ; :: according to TARSKI:def 3 :: thesis: ( not x in ((Seg (k + 1)) \ {i}) \/ {g} or x in (Seg g) \ {i} )
assume A58: x in ((Seg (k + 1)) \ {i}) \/ {g} ; :: thesis: x in (Seg g) \ {i}

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

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

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

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

end;

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

then A65: x = g by TARSKI:def 1;
1 <= g by A9, A12, XXREAL_0:2;
hence x in (Seg g) \ {i} by A27, A28, A65; :: 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 {g} c= Seg g by A13;
then {g} is included_in_Seg by FINSEQ_1:def 13;
then A67: Sgm ((Seg g) \ {i}) = (Sgm ((Seg (k + 1)) \ {i})) ^ (Sgm {g}) by A52, A48, Th40;
n <= k by A47, NAT_1:13;
then A68: n in Seg k by A11, FINSEQ_1:1;
A69: i in Seg (k + 1) by A9, A44, FINSEQ_1:1;
then len (Sgm ((Seg (k + 1)) \ {i})) = k by Th105;
then A70: n in dom (Sgm ((Seg (k + 1)) \ {i})) by A68, FINSEQ_1:def 3;
n <= k by A47, NAT_1:13;
then A71: n in Seg k by A11, FINSEQ_1:1;
then A72: ( 1 <= n & n < i implies (Sgm ((Seg (k + 1)) \ {i})) . n = n ) by A5, A69;

now :: thesis: ( 1 <= n & n < i implies (Sgm ((Seg g) \ {i})) . n = n )

assume that
A73: 1 <= n and
A74: n < i ; :: thesis: (Sgm ((Seg g) \ {i})) . n = n
n in Seg (len (Sgm ((Seg (k + 1)) \ {i}))) by A71, A69, Th105;
then n in dom (Sgm ((Seg (k + 1)) \ {i})) by FINSEQ_1:def 3;
hence (Sgm ((Seg g) \ {i})) . n = n by A72, A67, A73, A74, 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
A75: 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, A71, A69;
hence (Sgm ((Seg g) \ {i})) . n = n + 1 by A47, A67, A75, A70, 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;

A76: S₁[ 0 ] ;
for k being Nat holds S₁[k] from NAT_1:sch 2(A76, 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