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 1 <= i & i <= k - 1 holds
(SgmX (R,B)) /. i = (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 1 <= i & i <= k - 1 holds
(SgmX (R,B)) /. i = (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 1 <= i & i <= k - 1 holds
(SgmX (R,B)) /. i = (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 1 <= i & i <= k - 1 holds
(SgmX (R,B)) /. i = (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 1 <= i & i <= k - 1 holds
(SgmX (R,B)) /. i = (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 1 <= i & i <= k - 1 holds
(SgmX (R,B)) /. i = (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 1 <= i & i <= k - 1 holds
(SgmX (R,B)) /. i = (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 1 <= i & i <= k - 1 holds
(SgmX (R,B)) /. i = (SgmX (R,A)) /. i
then A4: R linearly_orders A by A2, Lm6;
field R = X by ORDERS_1:12;
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;
consider lensgb being Nat such that
A7: dom (SgmX (R,B)) = Seg lensgb by FINSEQ_1:def 2;
reconsider lensga = lensga, lensgb = lensgb as Element of NAT by ORDINAL1:def 12;
lensgb = len (SgmX (R,B)) by A7, FINSEQ_1:def 3
.= card B by A3, Th10
.= (card A) + 1 by A1, A2, CARD_2:41
.= (len (SgmX (R,A))) + 1 by A2, A3, Lm6, Th10
.= lensga + 1 by A6, FINSEQ_1:def 3 ;
then A8: lensga <= lensgb by NAT_1:11;
defpred S₁[ Nat] means (SgmX (R,B)) /. $1 = (SgmX (R,A)) /. $1;
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 1 <= i & i <= k - 1 holds
(SgmX (R,B)) /. i = (SgmX (R,A)) /. i )
assume that
A9: k in dom (SgmX (R,B)) and
A10: (SgmX (R,B)) /. k = a ; :: thesis: for i being Element of NAT st 1 <= i & i <= k - 1 holds
(SgmX (R,B)) /. i = (SgmX (R,A)) /. i
k in Seg (len (SgmX (R,B))) by A9, FINSEQ_1:def 3;
then A11: 1 <= k by FINSEQ_1:1;
then 1 - 1 <= k - 1 by XREAL_1:9;
then reconsider k9 = k - 1 as Element of NAT by INT_1:3;
A12: (k - 1) + 1 = k + 0 ;
A13: for j being Element of NAT st 1 <= j & j < k9 & ( for j9 being Element of NAT st 1 <= j9 & j9 <= j holds
S₁[j9] ) holds
S₁[j + 1]

proof

let i9 be Element of NAT ; :: thesis: ( 1 <= i9 & i9 < k9 & ( for j9 being Element of NAT st 1 <= j9 & j9 <= i9 holds
S₁[j9] ) implies S₁[i9 + 1] )
assume that
A14: 1 <= i9 and
A15: i9 < k9 ; :: thesis: ( ex j9 being Element of NAT st
( 1 <= j9 & j9 <= i9 & not S₁[j9] ) or S₁[i9 + 1] )
A16: 1 <= i9 + 1 by A14, XREAL_1:29;
A17: i9 + 1 < k by A12, A15, XREAL_1:6;
then A18: i9 + 1 in dom (SgmX (R,B)) by A9, A16, FINSEQ_3:156;
(SgmX (R,B)) /. (i9 + 1) = (SgmX (R,B)) . (i9 + 1) by A9, A17, A16, FINSEQ_3:156, PARTFUN1:def 6;
then (SgmX (R,B)) /. (i9 + 1) in rng (SgmX (R,B)) by A18, FUNCT_1:def 3;
then A19: (SgmX (R,B)) /. (i9 + 1) in B by A3, Def2;
(SgmX (R,B)) /. (i9 + 1) <> a by A3, A9, A10, A17, A18, Def2;
then not (SgmX (R,B)) /. (i9 + 1) in {a} by TARSKI:def 1;
then (SgmX (R,B)) /. (i9 + 1) in A by A2, A19, XBOOLE_0:def 3;
then (SgmX (R,B)) /. (i9 + 1) in rng (SgmX (R,A)) by A4, Def2;
then consider l being object such that
A20: l in dom (SgmX (R,A)) and
A21: (SgmX (R,A)) . l = (SgmX (R,B)) /. (i9 + 1) by FUNCT_1:def 3;
reconsider l = l as Element of NAT by A20;
A22: 1 <= l by A6, A20, FINSEQ_1:1;
l <= lensga by A6, A20, FINSEQ_1:1;
then l <= lensgb by A8, XXREAL_0:2;
then A23: l in dom (SgmX (R,B)) by A7, A22, FINSEQ_1:1;
assume A24: for j9 being Element of NAT st 1 <= j9 & j9 <= i9 holds
S₁[j9] ; :: thesis: S₁[i9 + 1]
assume A25: (SgmX (R,B)) /. (i9 + 1) <> (SgmX (R,A)) /. (i9 + 1) ; :: thesis: contradiction
then A26: l <> i9 + 1 by A20, A21, PARTFUN1:def 6;

per cases ( l < i9 + 1 or i9 + 1 <= l ) ;

suppose l < i9 + 1 ; :: thesis: contradiction

then l <= i9 by NAT_1:13;
then (SgmX (R,B)) /. l = (SgmX (R,A)) /. l by A24, A22
.= (SgmX (R,B)) /. (i9 + 1) by A20, A21, PARTFUN1:def 6 ;
hence contradiction by A3, A18, A26, A23, Th75; :: thesis: verum

end;

suppose A27: i9 + 1 <= l ; :: thesis: contradiction

then A28: i9 + 1 in dom (SgmX (R,A)) by A16, A20, FINSEQ_3:156;
(SgmX (R,A)) /. (i9 + 1) = (SgmX (R,A)) . (i9 + 1) by A16, A20, A27, FINSEQ_3:156, PARTFUN1:def 6;
then (SgmX (R,A)) /. (i9 + 1) in rng (SgmX (R,A)) by A28, FUNCT_1:def 3;
then (SgmX (R,A)) /. (i9 + 1) in A by A4, Def2;
then (SgmX (R,A)) /. (i9 + 1) in B by A2, XBOOLE_0:def 3;
then (SgmX (R,A)) /. (i9 + 1) in rng (SgmX (R,B)) by A3, Def2;
then consider l9 being object such that
A29: l9 in dom (SgmX (R,B)) and
A30: (SgmX (R,B)) . l9 = (SgmX (R,A)) /. (i9 + 1) by FUNCT_1:def 3;
reconsider l9 = l9 as Element of NAT by A29;
i9 + 1 < l by A26, A27, XXREAL_0:1;
then [((SgmX (R,A)) /. (i9 + 1)),((SgmX (R,A)) /. l)] in R by A4, A20, A28, Def2;
then [((SgmX (R,B)) /. l9),((SgmX (R,A)) /. l)] in R by A29, A30, PARTFUN1:def 6;
then A31: [((SgmX (R,B)) /. l9),((SgmX (R,B)) /. (i9 + 1))] in R by A20, A21, PARTFUN1:def 6;
(SgmX (R,B)) /. l9 = (SgmX (R,B)) . l9 by A29, PARTFUN1:def 6;
then (SgmX (R,B)) /. l9 in rng (SgmX (R,B)) by A29, FUNCT_1:def 3;
then A32: (SgmX (R,B)) /. l9 in B by A3, Def2;
A33: 1 <= l9 by A7, A29, FINSEQ_1:1;
A34: i9 + 1 < l9

proof

assume A35: l9 <= i9 + 1 ; :: thesis: contradiction

now :: thesis: ( ( l9 = i9 + 1 & contradiction ) or ( l9 < i9 + 1 & contradiction ) )

per cases ( l9 = i9 + 1 or l9 < i9 + 1 ) by A35, XXREAL_0:1;

case l9 = i9 + 1 ; :: thesis: contradiction

hence contradiction by A25, A29, A30, PARTFUN1:def 6; :: thesis: verum

end;

case A36: l9 < i9 + 1 ; :: thesis: contradiction

then l9 <= i9 by NAT_1:13;
then A37: (SgmX (R,A)) /. l9 = (SgmX (R,B)) /. l9 by A24, A33
.= (SgmX (R,A)) /. (i9 + 1) by A29, A30, PARTFUN1:def 6 ;
l9 in dom (SgmX (R,A)) by A28, A33, A36, FINSEQ_3:156;
hence contradiction by A2, A3, A28, A36, A37, Lm6, Th75; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

then [((SgmX (R,B)) /. (i9 + 1)),((SgmX (R,B)) /. l9)] in R by A3, A18, A29, Def2;
then (SgmX (R,B)) /. l9 = (SgmX (R,B)) /. (i9 + 1) by A5, A31, A32;
hence contradiction by A3, A18, A29, A34, Th75; :: thesis: verum

end;

end;

end;

let i be Element of NAT ; :: thesis: ( 1 <= i & i <= k - 1 implies (SgmX (R,B)) /. i = (SgmX (R,A)) /. i )
assume that
A38: 1 <= i and
A39: i <= k - 1 ; :: thesis: (SgmX (R,B)) /. i = (SgmX (R,A)) /. i
A40: 1 in dom (SgmX (R,B)) by A9, Lm5;
A41: S₁[1]

proof

(SgmX (R,B)) /. 1 = (SgmX (R,B)) . 1 by A9, Lm5, PARTFUN1:def 6;
then (SgmX (R,B)) /. 1 in rng (SgmX (R,B)) by A40, FUNCT_1:def 3;
then A42: (SgmX (R,B)) /. 1 in B by A3, Def2;
k <> 1 by A38, A39, XXREAL_0:2;
then 1 < k by A11, XXREAL_0:1;
then (SgmX (R,B)) /. 1 <> a by A3, A9, A10, A40, Def2;
then not (SgmX (R,B)) /. 1 in {a} by TARSKI:def 1;
then (SgmX (R,B)) /. 1 in A by A2, A42, XBOOLE_0:def 3;
then (SgmX (R,B)) /. 1 in rng (SgmX (R,A)) by A4, Def2;
then consider l being object such that
A43: l in dom (SgmX (R,A)) and
A44: (SgmX (R,A)) . l = (SgmX (R,B)) /. 1 by FUNCT_1:def 3;
A45: (SgmX (R,A)) /. 1 = (SgmX (R,A)) . 1 by A43, Lm5, PARTFUN1:def 6;
assume A46: (SgmX (R,B)) /. 1 <> (SgmX (R,A)) /. 1 ; :: thesis: contradiction
reconsider l = l as Element of NAT by A43;
A47: 1 in dom (SgmX (R,A)) by A43, Lm5;
1 <= l by A6, A43, FINSEQ_1:1;
then 1 < l by A46, A44, A45, XXREAL_0:1;
then [((SgmX (R,A)) /. 1),((SgmX (R,A)) /. l)] in R by A4, A43, A47, Def2;
then A48: [((SgmX (R,A)) /. 1),((SgmX (R,B)) /. 1)] in R by A43, A44, PARTFUN1:def 6;
not (SgmX (R,A)) /. 1 in B

proof

A49: (SgmX (R,B)) /. 1 = (SgmX (R,B)) . 1 by A9, Lm5, PARTFUN1:def 6;
assume (SgmX (R,A)) /. 1 in B ; :: thesis: contradiction
then (SgmX (R,A)) /. 1 in rng (SgmX (R,B)) by A3, Def2;
then consider l9 being object such that
A50: l9 in dom (SgmX (R,B)) and
A51: (SgmX (R,B)) . l9 = (SgmX (R,A)) /. 1 by FUNCT_1:def 3;
reconsider l9 = l9 as Element of NAT by A50;
1 <= l9 by A7, A50, FINSEQ_1:1;
then 1 < l9 by A46, A51, A49, XXREAL_0:1;
then [((SgmX (R,B)) /. 1),((SgmX (R,B)) /. l9)] in R by A3, A40, A50, Def2;
then [((SgmX (R,B)) /. 1),((SgmX (R,A)) /. 1)] in R by A50, A51, PARTFUN1:def 6;
hence contradiction by A5, A46, A42, A48; :: thesis: verum

end;

then A52: not (SgmX (R,A)) /. 1 in A by A2, XBOOLE_0:def 3;
(SgmX (R,A)) /. 1 in rng (SgmX (R,A)) by A47, A45, FUNCT_1:def 3;
hence contradiction by A4, A52, Def2; :: thesis: verum

end;

for j being Element of NAT st 1 <= j & j <= k9 holds
S₁[j] from INT_1:sch 8(A41, A13);
hence (SgmX (R,B)) /. i = (SgmX (R,A)) /. i by A38, A39; :: thesis: verum