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, 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;
defpred S1[ 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:1;
then 1 - 1 <= k - 1 by XREAL_1:9;
then reconsider k9 = k - 1 as Element of NAT by INT_1:3;
reconsider lensga = lensga, lensgb = lensgb as Element of NAT by ORDINAL1:def 12;
A11: k9 + 1 = k + 0 ;
A12: 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 ;
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
S1[j9] ) holds
S1[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
S1[j9] ) implies S1[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 S1[j9] ) or S1[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, Th10
.= (card A) + 1 by A1, A2, CARD_2:41
.= (len (SgmX (R,A))) + 1 by A2, A3, Lm6, Th10 ;
then j + 1 < len (SgmX (R,B)) by A15, XREAL_1:6;
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:1;
now :: thesis: not (SgmX (R,B)) /. (j + 2) = a
assume (SgmX (R,B)) /. (j + 2) = a ; :: thesis: contradiction
then j + 2 = k by A3, A8, A9, A18, Th75;
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 6;
then (SgmX (R,B)) /. (j + 2) in rng (SgmX (R,B)) by A18, FUNCT_1:def 3;
then (SgmX (R,B)) /. (j + 2) in B by A3, Def2;
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, Def2;
then consider l being object such that
A20: l in dom (SgmX (R,A)) and
A21: (SgmX (R,A)) . l = (SgmX (R,B)) /. (j + 2) by FUNCT_1:def 3;
reconsider l = l as Element of NAT by A20;
A22: (SgmX (R,A)) /. l = (SgmX (R,A)) . l by A20, PARTFUN1:def 6;
A23: 1 <= l by A6, A20, FINSEQ_1:1;
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:1;
then A26: (SgmX (R,A)) /. (j + 1) = (SgmX (R,A)) . (j + 1) by PARTFUN1:def 6;
assume A27: for j9 being Element of NAT st k <= j9 & j9 <= j holds
S1[j9] ; :: thesis: S1[j + 1]
l <= lensga by A6, A20, FINSEQ_1:1;
then A28: l + 1 <= lensgb by A12, XREAL_1:6;
1 <= l + 1 by NAT_1:12;
then A29: l + 1 in dom (SgmX (R,B)) by A7, A28, FINSEQ_1:1;
l <= l + 1 by XREAL_1:29;
then A30: l in dom (SgmX (R,B)) by A23, A29, FINSEQ_3:156;
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 6;
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 :: thesis: ( ( k <= l & contradiction ) or ( l < k & contradiction ) )
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, Th75, PARTFUN1:def 6;
hence contradiction by A31, A20, A21, PARTFUN1:def 6; :: 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, Th76;
j + 1 < (j + 1) + 1 by XREAL_1:29;
hence contradiction by A3, A18, A20, A21, A30, A33, A35, Th75, PARTFUN1:def 6; :: 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 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:1;
now :: thesis: ( ( i9 <= k & contradiction ) or ( k < i9 & contradiction ) )
per cases ( i9 <= k or k < i9 ) ;
case A44: i9 <= k ; :: thesis: contradiction
now :: thesis: ( ( i9 = k & contradiction ) or ( i9 <> k & contradiction ) )
per cases ( i9 = k or i9 <> k ) ;
end;
end;
hence contradiction ; :: thesis: verum
end;
case A46: k < i9 ; :: thesis: contradiction
A47: i9 - 1 <= (j + 1) - 1 by A42, XREAL_1:9;
A48: i9 - 1 <= i9 by XREAL_1:146;
1 <= i9 by A10, A46, XXREAL_0:2;
then 1 - 1 <= i9 - 1 by XREAL_1:9;
then A49: i9 - 1 is Element of NAT by INT_1:3;
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, FINSEQ_3:156;
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, Lm6, Th75; :: 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 3;
then A52: (SgmX (R,A)) /. (j + 1) in A by A4, Def2;
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, Def2;
then consider l9 being object such that
A53: l9 in dom (SgmX (R,B)) and
A54: (SgmX (R,B)) . l9 = (SgmX (R,A)) /. (j + 1) by FUNCT_1:def 3;
reconsider l9 = l9 as Element of NAT by A53;
A55: (SgmX (R,B)) /. l9 = (SgmX (R,B)) . l9 by A53, PARTFUN1:def 6;
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:1;
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, Def2;
1 <= l9 by A7, A53, FINSEQ_1:1;
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, Def2;
then (SgmX (R,A)) /. l = (SgmX (R,A)) /. (j + 1) by A5, A57, A52;
hence contradiction by A2, A3, A25, A20, A36, Lm6, Th75; :: 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:1;
A62: lensga <= lensgb by A12, NAT_1:11;
A63: S1[k]
proof
A64: (SgmX (R,A)) /. k = (SgmX (R,A)) . k by A61, PARTFUN1:def 6;
then (SgmX (R,A)) /. k in rng (SgmX (R,A)) by A61, FUNCT_1:def 3;
then (SgmX (R,A)) /. k in A by A4, Def2;
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, Def2;
then consider l being object such that
A65: l in dom (SgmX (R,B)) and
A66: (SgmX (R,B)) . l = (SgmX (R,A)) /. k by FUNCT_1:def 3;
reconsider l = l as Element of NAT by A65;
A67: (SgmX (R,B)) /. l = (SgmX (R,B)) . l by A65, PARTFUN1:def 6;
A68: 1 <= l by A7, A65, FINSEQ_1:1;
assume A69: not S1[k] ; :: thesis: contradiction
then A70: l <> k + 1 by A65, A66, PARTFUN1:def 6;
per cases ( l = k or l < k or k < l ) by XXREAL_0:1;
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:1;
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, Th76;
hence contradiction by A2, A3, A61, A71, A72, Lm6, Th75; :: 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, FINSEQ_3:156;
now :: thesis: not (SgmX (R,B)) /. (k + 1) = a
assume (SgmX (R,B)) /. (k + 1) = a ; :: thesis: contradiction
then k + 1 = k by A3, A8, A9, A75, Th75;
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, Def2;
(SgmX (R,B)) /. l in rng (SgmX (R,B)) by A65, A67, FUNCT_1:def 3;
then A78: (SgmX (R,B)) /. l in B by A3, Def2;
(SgmX (R,B)) /. (k + 1) = (SgmX (R,B)) . (k + 1) by A65, A73, A74, FINSEQ_3:156, PARTFUN1:def 6;
then (SgmX (R,B)) /. (k + 1) in rng (SgmX (R,B)) by A75, FUNCT_1:def 3;
then (SgmX (R,B)) /. (k + 1) in B by A3, Def2;
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, Def2;
then consider l9 being object such that
A79: l9 in dom (SgmX (R,A)) and
A80: (SgmX (R,A)) . l9 = (SgmX (R,B)) /. (k + 1) by FUNCT_1:def 3;
reconsider l9 = l9 as Element of NAT by A79;
A81: (SgmX (R,A)) /. l9 = (SgmX (R,A)) . l9 by A79, PARTFUN1:def 6;
A82: 1 <= l9 by A6, A79, FINSEQ_1:1;
l9 <= lensga by A6, A79, FINSEQ_1:1;
then l9 <= lensgb by A62, XXREAL_0:2;
then A83: l9 in dom (SgmX (R,B)) by A7, A82, FINSEQ_1:1;
now :: thesis: not l9 < k
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, Th76;
then l9 = k + 1 by A3, A75, A79, A80, A83, Th75, PARTFUN1:def 6;
hence contradiction by A84, XREAL_1:29; :: 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, Def2;
then (SgmX (R,B)) /. l = (SgmX (R,B)) /. (k + 1) by A5, A77, A78;
hence contradiction by A69, A65, A66, PARTFUN1:def 6; :: thesis: verum
end;
end;
end;
for j being Element of NAT st k <= j & j <= len (SgmX (R,A)) holds
S1[j] from INT_1:sch 8(A63, A13);
 hence (SgmX (R,B)) /. (i + 1) = (SgmX (R,A)) /. i by A58, A59; :: thesis: verum