let X be set ; :: thesis: for A being finite Subset of X
for a being Element of X st not a in A holds
for B being finite Subset of X st B = {a} \/ A holds
for R being Order of X st R linearly_orders B holds
for k being Element of NAT st k in dom (SgmX R,B) & (SgmX R,B) /. k = a holds
for i being Element of NAT st k <= i & i <= len (SgmX R,A) holds
(SgmX R,B) /. (i + 1) = (SgmX R,A) /. i
let A be finite Subset of X; :: thesis: for a being Element of X st not a in A holds
for B being finite Subset of X st B = {a} \/ A holds
for R being Order of X st R linearly_orders B holds
for k being Element of NAT st k in dom (SgmX R,B) & (SgmX R,B) /. k = a holds
for i being Element of NAT st k <= i & i <= len (SgmX R,A) holds
(SgmX R,B) /. (i + 1) = (SgmX R,A) /. i
let a be Element of X; :: thesis: ( not a in A implies for B being finite Subset of X st B = {a} \/ A holds
for R being Order of X st R linearly_orders B holds
for k being Element of NAT st k in dom (SgmX R,B) & (SgmX R,B) /. k = a holds
for i being Element of NAT st k <= i & i <= len (SgmX R,A) holds
(SgmX R,B) /. (i + 1) = (SgmX R,A) /. i )
assume A1: not a in A ; :: thesis: for B being finite Subset of X st B = {a} \/ A holds
for R being Order of X st R linearly_orders B holds
for k being Element of NAT st k in dom (SgmX R,B) & (SgmX R,B) /. k = a holds
for i being Element of NAT st k <= i & i <= len (SgmX R,A) holds
(SgmX R,B) /. (i + 1) = (SgmX R,A) /. i
let B be finite Subset of X; :: thesis: ( B = {a} \/ A implies for R being Order of X st R linearly_orders B holds
for k being Element of NAT st k in dom (SgmX R,B) & (SgmX R,B) /. k = a holds
for i being Element of NAT st k <= i & i <= len (SgmX R,A) holds
(SgmX R,B) /. (i + 1) = (SgmX R,A) /. i )
assume A2: B = {a} \/ A ; :: thesis: for R being Order of X st R linearly_orders B holds
for k being Element of NAT st k in dom (SgmX R,B) & (SgmX R,B) /. k = a holds
for i being Element of NAT st k <= i & i <= len (SgmX R,A) holds
(SgmX R,B) /. (i + 1) = (SgmX R,A) /. i
let R be Order of X; :: thesis: ( R linearly_orders B implies for k being Element of NAT st k in dom (SgmX R,B) & (SgmX R,B) /. k = a holds
for i being Element of NAT st k <= i & i <= len (SgmX R,A) holds
(SgmX R,B) /. (i + 1) = (SgmX R,A) /. i )
assume A3: R linearly_orders B ; :: thesis: for k being Element of NAT st k in dom (SgmX R,B) & (SgmX R,B) /. k = a holds
for i being Element of NAT st k <= i & i <= len (SgmX R,A) holds
(SgmX R,B) /. (i + 1) = (SgmX R,A) /. i
then A4: R linearly_orders A by A2, Lm4;
field R = X by ORDERS_1:97;
then A5: R is_antisymmetric_in X by RELAT_2:def 12;
set sgb = SgmX R,B;
set sga = SgmX R,A;
consider lensga being Nat such that
A6: dom (SgmX R,A) = Seg lensga by FINSEQ_1:def 2;
defpred S₁[ Element of NAT ] means (SgmX R,B) /. ($1 + 1) = (SgmX R,A) /. $1;
consider lensgb being Nat such that
A7: dom (SgmX R,B) = Seg lensgb by FINSEQ_1:def 2;
let k be Element of NAT ; :: thesis: ( k in dom (SgmX R,B) & (SgmX R,B) /. k = a implies for i being Element of NAT st k <= i & i <= len (SgmX R,A) holds
(SgmX R,B) /. (i + 1) = (SgmX R,A) /. i )
assume that
A8: k in dom (SgmX R,B) and
A9: (SgmX R,B) /. k = a ; :: thesis: for i being Element of NAT st k <= i & i <= len (SgmX R,A) holds
(SgmX R,B) /. (i + 1) = (SgmX R,A) /. i
k in Seg (len (SgmX R,B)) by A8, FINSEQ_1:def 3;
then A10: 1 <= k by FINSEQ_1:3;
then 1 - 1 <= k - 1 by XREAL_1:11;
then reconsider k9 = k - 1 as Element of NAT by INT_1:16;
reconsider lensga = lensga, lensgb = lensgb as Element of NAT by ORDINAL1:def 13;
A11: k9 + 1 = k + 0 ;
A12: lensgb = len (SgmX R,B) by A7, FINSEQ_1:def 3
.= card B by A3, PRE_POLY:11
.= (card A) + 1 by A1, A2, CARD_2:54
.= (len (SgmX R,A)) + 1 by A2, A3, Lm4, PRE_POLY:11
.= lensga + 1 by A6, FINSEQ_1:def 3 ;
A13: for j being Element of NAT st k <= j & j < len (SgmX R,A) & ( for j9 being Element of NAT st k <= j9 & j9 <= j holds
S₁[j9] ) holds
S₁[j + 1]

proof

let j be Element of NAT ; :: thesis: ( k <= j & j < len (SgmX R,A) & ( for j9 being Element of NAT st k <= j9 & j9 <= j holds
S₁[j9] ) implies S₁[j + 1] )
assume that
A14: k <= j and
A15: j < len (SgmX R,A) ; :: thesis: ( ex j9 being Element of NAT st
( k <= j9 & j9 <= j & not S₁[j9] ) or S₁[j + 1] )
A16: (j + 1) + 1 = j + (1 + 1) ;
A17: 1 <= j + 2 by NAT_1:12;
len (SgmX R,B) = card B by A3, PRE_POLY:11
.= (card A) + 1 by A1, A2, CARD_2:54
.= (len (SgmX R,A)) + 1 by A2, A3, Lm4, PRE_POLY:11 ;
then j + 1 < len (SgmX R,B) by A15, XREAL_1:8;
then j + 2 <= len (SgmX R,B) by A16, NAT_1:13;
then j + 2 <= lensgb by A7, FINSEQ_1:def 3;
then A18: j + 2 in dom (SgmX R,B) by A7, A17, FINSEQ_1:3;

now

assume (SgmX R,B) /. (j + 2) = a ; :: thesis: contradiction
then j + 2 = k by A3, A8, A9, A18, Th10;
hence contradiction by A14, NAT_1:19; :: thesis: verum

end;

then A19: not (SgmX R,B) /. (j + 2) in {a} by TARSKI:def 1;
(SgmX R,B) /. (j + 2) = (SgmX R,B) . (j + 2) by A18, PARTFUN1:def 8;
then (SgmX R,B) /. (j + 2) in rng (SgmX R,B) by A18, FUNCT_1:def 5;
then (SgmX R,B) /. (j + 2) in B by A3, PRE_POLY:def 2;
then (SgmX R,B) /. (j + 2) in A by A2, A19, XBOOLE_0:def 3;
then (SgmX R,B) /. (j + 2) in rng (SgmX R,A) by A4, PRE_POLY:def 2;
then consider l being set such that
A20: l in dom (SgmX R,A) and
A21: (SgmX R,A) . l = (SgmX R,B) /. (j + 2) by FUNCT_1:def 5;
reconsider l = l as Element of NAT by A20;
A22: (SgmX R,A) /. l = (SgmX R,A) . l by A20, PARTFUN1:def 8;
A23: 1 <= l by A6, A20, FINSEQ_1:3;
j + 1 <= len (SgmX R,A) by A15, NAT_1:13;
then A24: j + 1 <= lensga by A6, FINSEQ_1:def 3;
1 <= j + 1 by NAT_1:12;
then A25: j + 1 in dom (SgmX R,A) by A6, A24, FINSEQ_1:3;
then A26: (SgmX R,A) /. (j + 1) = (SgmX R,A) . (j + 1) by PARTFUN1:def 8;
assume A27: for j9 being Element of NAT st k <= j9 & j9 <= j holds
S₁[j9] ; :: thesis: S₁[j + 1]
l <= lensga by A6, A20, FINSEQ_1:3;
then A28: l + 1 <= lensgb by A12, XREAL_1:8;
1 <= l + 1 by NAT_1:12;
then A29: l + 1 in dom (SgmX R,B) by A7, A28, FINSEQ_1:3;
l <= l + 1 by XREAL_1:31;
then A30: l in dom (SgmX R,B) by A23, A29, Th4;
assume A31: (SgmX R,B) /. ((j + 1) + 1) <> (SgmX R,A) /. (j + 1) ; :: thesis: contradiction
then A32: l <> j + 1 by A20, A21, PARTFUN1:def 8;

per cases ( l <= j + 1 or l > j + 1 ) ;

suppose A33: l <= j + 1 ; :: thesis: contradiction

then l < j + 1 by A32, XXREAL_0:1;
then A34: l <= j by NAT_1:13;

now

per cases ( k <= l or l < k ) ;

case k <= l ; :: thesis: contradiction

then (SgmX R,B) /. (l + 1) = (SgmX R,A) /. l by A27, A34;
then j + 2 = l + 1 by A3, A18, A20, A21, A29, Th10, PARTFUN1:def 8;
hence contradiction by A31, A20, A21, PARTFUN1:def 8; :: thesis: verum

end;

case l < k ; :: thesis: contradiction

then l <= k9 by A11, NAT_1:13;
then A35: (SgmX R,B) /. l = (SgmX R,A) /. l by A1, A2, A3, A8, A9, A23, Th11;
j + 1 < (j + 1) + 1 by XREAL_1:31;
hence contradiction by A3, A18, A20, A21, A30, A33, A35, Th10, PARTFUN1:def 8; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

suppose A36: l > j + 1 ; :: thesis: contradiction

A37: for i9 being Element of NAT st 1 <= i9 & i9 <= j + 2 holds
(SgmX R,A) /. (j + 1) <> (SgmX R,B) /. i9

proof

let i9 be Element of NAT ; :: thesis: ( 1 <= i9 & i9 <= j + 2 implies (SgmX R,A) /. (j + 1) <> (SgmX R,B) /. i9 )
assume that
A38: 1 <= i9 and
A39: i9 <= j + 2 ; :: thesis: (SgmX R,A) /. (j + 1) <> (SgmX R,B) /. i9
assume A40: (SgmX R,A) /. (j + 1) = (SgmX R,B) /. i9 ; :: thesis: contradiction

per cases ( i9 = j + 2 or i9 <> j + 2 ) ;

suppose i9 = j + 2 ; :: thesis: contradiction

hence contradiction by A31, A40; :: thesis: verum

end;

suppose A41: i9 <> j + 2 ; :: thesis: contradiction

then i9 < j + 2 by A39, XXREAL_0:1;
then A42: i9 <= j + 1 by A16, NAT_1:13;
then i9 <= lensga by A24, XXREAL_0:2;
then A43: i9 in dom (SgmX R,A) by A6, A38, FINSEQ_1:3;

now

per cases ( i9 <= k or k < i9 ) ;

case A44: i9 <= k ; :: thesis: contradiction

now

per cases ( i9 = k or i9 <> k ) ;

case i9 = k ; :: thesis: contradiction

then (SgmX R,A) . (j + 1) = a by A9, A25, A40, PARTFUN1:def 8;
then a in rng (SgmX R,A) by A25, FUNCT_1:def 5;
hence contradiction by A1, A4, PRE_POLY:def 2; :: thesis: verum

end;

case i9 <> k ; :: thesis: contradiction

then i9 < k by A44, XXREAL_0:1;
then i9 <= k9 by A11, NAT_1:13;
then (SgmX R,B) /. i9 = (SgmX R,A) /. i9 by A1, A2, A3, A8, A9, A38, Th11;
then A45: i9 = j + 1 by A2, A3, A25, A40, A43, Lm4, Th10;
i9 <= j by A14, A44, XXREAL_0:2;
hence contradiction by A45, XREAL_1:31; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

case A46: k < i9 ; :: thesis: contradiction

A47: i9 - 1 <= (j + 1) - 1 by A42, XREAL_1:11;
A48: i9 - 1 <= i9 by XREAL_1:148;
1 <= i9 by A10, A46, XXREAL_0:2;
then 1 - 1 <= i9 - 1 by XREAL_1:11;
then A49: i9 - 1 is Element of NAT by INT_1:16;
A50: (i9 - 1) + 1 = i9 + 0 ;
then k <= i9 - 1 by A46, A49, NAT_1:13;
then 1 <= i9 - 1 by A10, XXREAL_0:2;
then A51: i9 - 1 in dom (SgmX R,A) by A43, A49, A48, Th4;
k <= i9 - 1 by A46, A49, A50, NAT_1:13;
then (SgmX R,A) /. (i9 - 1) = (SgmX R,A) /. (j + 1) by A27, A40, A49, A50, A47;
hence contradiction by A2, A3, A16, A25, A41, A50, A51, Lm4, Th10; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

end;

end;

(SgmX R,A) /. (j + 1) in rng (SgmX R,A) by A25, A26, FUNCT_1:def 5;
then A52: (SgmX R,A) /. (j + 1) in A by A4, PRE_POLY:def 2;
then (SgmX R,A) /. (j + 1) in B by A2, XBOOLE_0:def 3;
then (SgmX R,A) /. (j + 1) in rng (SgmX R,B) by A3, PRE_POLY:def 2;
then consider l9 being set such that
A53: l9 in dom (SgmX R,B) and
A54: (SgmX R,B) . l9 = (SgmX R,A) /. (j + 1) by FUNCT_1:def 5;
reconsider l9 = l9 as Element of NAT by A53;
A55: (SgmX R,B) /. l9 = (SgmX R,B) . l9 by A53, PARTFUN1:def 8;
A56: 1 <= j + 1 by NAT_1:12;
j + 1 <= len (SgmX R,A) by A15, NAT_1:13;
then j + 1 in Seg (len (SgmX R,A)) by A56, FINSEQ_1:3;
then j + 1 in dom (SgmX R,A) by FINSEQ_1:def 3;
then A57: [((SgmX R,A) /. (j + 1)),((SgmX R,A) /. l)] in R by A4, A20, A36, PRE_POLY:def 2;
1 <= l9 by A7, A53, FINSEQ_1:3;
then l9 > j + 2 by A37, A54, A55;
then [((SgmX R,A) /. l),((SgmX R,A) /. (j + 1))] in R by A3, A18, A21, A22, A53, A54, A55, PRE_POLY:def 2;
then (SgmX R,A) /. l = (SgmX R,A) /. (j + 1) by A5, A57, A52, RELAT_2:def 4;
hence contradiction by A2, A3, A25, A20, A36, Lm4, Th10; :: thesis: verum

end;

end;

end;

let i be Element of NAT ; :: thesis: ( k <= i & i <= len (SgmX R,A) implies (SgmX R,B) /. (i + 1) = (SgmX R,A) /. i )
assume that
A58: k <= i and
A59: i <= len (SgmX R,A) ; :: thesis: (SgmX R,B) /. (i + 1) = (SgmX R,A) /. i
k <= len (SgmX R,A) by A58, A59, XXREAL_0:2;
then A60: k <= lensga by A6, FINSEQ_1:def 3;
then A61: k in dom (SgmX R,A) by A10, A6, FINSEQ_1:3;
A62: lensga <= lensgb by A12, NAT_1:11;
A63: S₁[k]

proof

A64: (SgmX R,A) /. k = (SgmX R,A) . k by A61, PARTFUN1:def 8;
then (SgmX R,A) /. k in rng (SgmX R,A) by A61, FUNCT_1:def 5;
then (SgmX R,A) /. k in A by A4, PRE_POLY:def 2;
then (SgmX R,A) /. k in B by A2, XBOOLE_0:def 3;
then (SgmX R,A) /. k in rng (SgmX R,B) by A3, PRE_POLY:def 2;
then consider l being set such that
A65: l in dom (SgmX R,B) and
A66: (SgmX R,B) . l = (SgmX R,A) /. k by FUNCT_1:def 5;
reconsider l = l as Element of NAT by A65;
A67: (SgmX R,B) /. l = (SgmX R,B) . l by A65, PARTFUN1:def 8;
A68: 1 <= l by A7, A65, FINSEQ_1:3;
assume A69: not S₁[k] ; :: thesis: contradiction
then A70: l <> k + 1 by A65, A66, PARTFUN1:def 8;

per cases ( l = k or l < k or k < l ) by XXREAL_0:1;

suppose l = k ; :: thesis: contradiction

then (SgmX R,A) . k = a by A8, A9, A64, A66, PARTFUN1:def 8;
then a in rng (SgmX R,A) by A61, FUNCT_1:def 5;
hence contradiction by A1, A4, PRE_POLY:def 2; :: thesis: verum

end;

suppose A71: l < k ; :: thesis: contradiction

then l <= lensga by A60, XXREAL_0:2;
then A72: l in dom (SgmX R,A) by A6, A68, FINSEQ_1:3;
l <= k9 by A11, A71, NAT_1:13;
then (SgmX R,A) /. l = (SgmX R,A) /. k by A1, A2, A3, A8, A9, A66, A68, A67, Th11;
hence contradiction by A2, A3, A61, A71, A72, Lm4, Th10; :: thesis: verum

end;

suppose k < l ; :: thesis: contradiction

then A73: k + 1 <= l by NAT_1:13;
A74: 1 <= k + 1 by NAT_1:12;
then A75: k + 1 in dom (SgmX R,B) by A65, A73, Th4;

now

assume (SgmX R,B) /. (k + 1) = a ; :: thesis: contradiction
then k + 1 = k by A3, A8, A9, A75, Th10;
hence contradiction ; :: thesis: verum

end;

then A76: not (SgmX R,B) /. (k + 1) in {a} by TARSKI:def 1;
k + 1 < l by A70, A73, XXREAL_0:1;
then A77: [((SgmX R,B) /. (k + 1)),((SgmX R,B) /. l)] in R by A3, A65, A75, PRE_POLY:def 2;
(SgmX R,B) /. l in rng (SgmX R,B) by A65, A67, FUNCT_1:def 5;
then A78: (SgmX R,B) /. l in B by A3, PRE_POLY:def 2;
(SgmX R,B) /. (k + 1) = (SgmX R,B) . (k + 1) by A65, A73, A74, Th4, PARTFUN1:def 8;
then (SgmX R,B) /. (k + 1) in rng (SgmX R,B) by A75, FUNCT_1:def 5;
then (SgmX R,B) /. (k + 1) in B by A3, PRE_POLY:def 2;
then (SgmX R,B) /. (k + 1) in A by A2, A76, XBOOLE_0:def 3;
then (SgmX R,B) /. (k + 1) in rng (SgmX R,A) by A4, PRE_POLY:def 2;
then consider l9 being set such that
A79: l9 in dom (SgmX R,A) and
A80: (SgmX R,A) . l9 = (SgmX R,B) /. (k + 1) by FUNCT_1:def 5;
reconsider l9 = l9 as Element of NAT by A79;
A81: (SgmX R,A) /. l9 = (SgmX R,A) . l9 by A79, PARTFUN1:def 8;
A82: 1 <= l9 by A6, A79, FINSEQ_1:3;
l9 <= lensga by A6, A79, FINSEQ_1:3;
then l9 <= lensgb by A62, XXREAL_0:2;
then A83: l9 in dom (SgmX R,B) by A7, A82, FINSEQ_1:3;

now

assume A84: l9 < k ; :: thesis: contradiction
then l9 <= k9 by A11, NAT_1:13;
then (SgmX R,B) /. l9 = (SgmX R,A) /. l9 by A1, A2, A3, A8, A9, A82, Th11;
then l9 = k + 1 by A3, A75, A79, A80, A83, Th10, PARTFUN1:def 8;
hence contradiction by A84, XREAL_1:31; :: thesis: verum

end;

then l9 > k by A69, A80, A81, XXREAL_0:1;
then [((SgmX R,B) /. l),((SgmX R,B) /. (k + 1))] in R by A4, A61, A66, A67, A79, A80, A81, PRE_POLY:def 2;
then (SgmX R,B) /. l = (SgmX R,B) /. (k + 1) by A5, A77, A78, RELAT_2:def 4;
hence contradiction by A69, A65, A66, PARTFUN1:def 8; :: thesis: verum

end;

end;

end;

for j being Element of NAT st k <= j & j <= len (SgmX R,A) holds
S₁[j] from POLYNOM2:sch 5(A63, A13);
hence (SgmX R,B) /. (i + 1) = (SgmX R,A) /. i by A58, A59; :: thesis: verum