let X be set ; 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; 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; ( 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
; 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; ( 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
; 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; ( 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
; 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 S1[ Nat] means (SgmX (R,B)) /. $1 = (SgmX (R,A)) /. $1;
let k be Element of NAT ; ( 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
; 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
S1[j9] ) holds
S1[j + 1]
proof
let i9 be
Element of
NAT ;
( 1 <= i9 & i9 < k9 & ( for j9 being Element of NAT st 1 <= j9 & j9 <= i9 holds
S1[j9] ) implies S1[i9 + 1] )
assume that A14:
1
<= i9
and A15:
i9 < k9
;
( ex j9 being Element of NAT st
( 1 <= j9 & j9 <= i9 & not S1[j9] ) or S1[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
S1[
j9]
;
S1[i9 + 1]
assume A25:
(SgmX (R,B)) /. (i9 + 1) <> (SgmX (R,A)) /. (i9 + 1)
;
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
;
contradictionthen
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;
verum end; suppose A27:
i9 + 1
<= l
;
contradictionthen 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
;
contradiction
now ( ( 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
;
contradictionend; case A36:
l9 < i9 + 1
;
contradictionthen
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;
verum end;
hence
contradiction
;
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;
verum end;
end;
let i be Element of NAT ; ( 1 <= i & i <= k - 1 implies (SgmX (R,B)) /. i = (SgmX (R,A)) /. i )
assume that
A38:
1 <= i
and
A39:
i <= k - 1
; (SgmX (R,B)) /. i = (SgmX (R,A)) /. i
A40:
1 in dom (SgmX (R,B))
by A9, Lm5;
A41:
S1[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
;
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
;
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;
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;
verum
end;
for j being Element of NAT st 1 <= j & j <= k9 holds
S1[j]
from INT_1:sch 8(A41, A13);
hence
(SgmX (R,B)) /. i = (SgmX (R,A)) /. i
by A38, A39; verum