let X be non empty set ; for A being finite Subset of X
for R being Order of X st R linearly_orders A holds
for i, k being Nat st 1 <= i & i <= k & k <= card A holds
(SgmX (R,(rng ((SgmX (R,A)) | k)))) /. i = (SgmX (R,A)) /. i
let A be finite Subset of X; for R being Order of X st R linearly_orders A holds
for i, k being Nat st 1 <= i & i <= k & k <= card A holds
(SgmX (R,(rng ((SgmX (R,A)) | k)))) /. i = (SgmX (R,A)) /. i
let R be Order of X; ( R linearly_orders A implies for i, k being Nat st 1 <= i & i <= k & k <= card A holds
(SgmX (R,(rng ((SgmX (R,A)) | k)))) /. i = (SgmX (R,A)) /. i )
assume A1:
R linearly_orders A
; for i, k being Nat st 1 <= i & i <= k & k <= card A holds
(SgmX (R,(rng ((SgmX (R,A)) | k)))) /. i = (SgmX (R,A)) /. i
set Sp = SgmX (R,A);
A2:
card A = len (SgmX (R,A))
by A1, PRE_POLY:11;
A3:
rng (SgmX (R,A)) = A
by A1, PRE_POLY:def 2;
defpred S1[ Nat] means for i being Nat st 1 <= i & i <= $1 & $1 <= card A holds
(SgmX (R,(rng ((SgmX (R,A)) | $1)))) /. i = (SgmX (R,A)) /. i;
A4:
S1[ 0 ]
;
A5:
for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
set k1 =
k + 1;
assume A6:
S1[
k]
;
S1[k + 1]
let i be
Nat;
( 1 <= i & i <= k + 1 & k + 1 <= card A implies (SgmX (R,(rng ((SgmX (R,A)) | (k + 1))))) /. i = (SgmX (R,A)) /. i )
assume A7:
( 1
<= i &
i <= k + 1 &
k + 1
<= card A )
;
(SgmX (R,(rng ((SgmX (R,A)) | (k + 1))))) /. i = (SgmX (R,A)) /. i
A8:
SgmX (
R,
A) is
one-to-one
by A1, PRE_POLY:10;
set Spk1 =
(SgmX (R,A)) | (k + 1);
A9:
k < card A
by A7, NAT_1:13;
then A10:
(
len ((SgmX (R,A)) | (k + 1)) = k + 1 &
len ((SgmX (R,A)) | k) = k )
by A7, A2, FINSEQ_1:59;
A11:
k < len (SgmX (R,A))
by A7, A2, NAT_1:13;
A12:
(SgmX (R,A)) | (k + 1) = ((SgmX (R,A)) | k) ^ <*((SgmX (R,A)) . (k + 1))*>
by A7, A2, NAT_1:13, FINSEQ_5:83;
A13:
R linearly_orders rng ((SgmX (R,A)) | (k + 1))
by A3, RELAT_1:70, A1, ORDERS_1:38;
A14:
1
<= k + 1
by NAT_1:11;
A15:
k + 1
in dom (SgmX (R,A))
by NAT_1:11, A7, A2, FINSEQ_3:25;
then A16:
(SgmX (R,A)) . (k + 1) in rng (SgmX (R,A))
by FUNCT_1:def 3;
A17:
(SgmX (R,A)) . (k + 1) = (SgmX (R,A)) /. (k + 1)
by A15, PARTFUN1:def 6;
A18:
k + 1
in Seg (k + 1)
by A14;
A19:
(SgmX (R,A)) /. (k + 1) in rng ((SgmX (R,A)) | (k + 1))
by A15, A18, PARTFUN2:18;
A20:
for
y being
Element of
X st
y in rng ((SgmX (R,A)) | (k + 1)) holds
[y,((SgmX (R,A)) /. (k + 1))] in R
proof
let y be
Element of
X;
( y in rng ((SgmX (R,A)) | (k + 1)) implies [y,((SgmX (R,A)) /. (k + 1))] in R )
assume A21:
y in rng ((SgmX (R,A)) | (k + 1))
;
[y,((SgmX (R,A)) /. (k + 1))] in R
consider w being
object such that A22:
(
w in dom ((SgmX (R,A)) | (k + 1)) &
((SgmX (R,A)) | (k + 1)) . w = y )
by A21, FUNCT_1:def 3;
reconsider w =
w as
Nat by A22;
A23:
( 1
<= w &
w <= k + 1 )
by A22, A10, FINSEQ_3:25;
then A24:
((SgmX (R,A)) | (k + 1)) . w = (SgmX (R,A)) . w
by FINSEQ_3:112;
w <= len (SgmX (R,A))
by A7, A2, A23, XXREAL_0:2;
then A25:
w in dom (SgmX (R,A))
by A23, FINSEQ_3:25;
then A26:
(SgmX (R,A)) /. w = (SgmX (R,A)) . w
by PARTFUN1:def 6;
end;
A28:
len (SgmX (R,(rng ((SgmX (R,A)) | (k + 1))))) =
card (rng ((SgmX (R,A)) | (k + 1)))
by A13, PRE_POLY:11
.=
k + 1
by A10, A8, FINSEQ_4:62
;
A29:
not
(SgmX (R,A)) /. (k + 1) in rng ((SgmX (R,A)) | k)
proof
assume
(SgmX (R,A)) /. (k + 1) in rng ((SgmX (R,A)) | k)
;
contradiction
then consider w being
object such that A30:
(
w in dom ((SgmX (R,A)) | k) &
((SgmX (R,A)) | k) . w = (SgmX (R,A)) /. (k + 1) )
by FUNCT_1:def 3;
reconsider w =
w as
Nat by A30;
A31:
( 1
<= w &
w <= k )
by A30, A10, FINSEQ_3:25;
w <= len (SgmX (R,A))
by A9, A2, A31, XXREAL_0:2;
then A32:
w in dom (SgmX (R,A))
by A31, FINSEQ_3:25;
(SgmX (R,A)) . w = (SgmX (R,A)) . (k + 1)
by A30, A31, FINSEQ_3:112, A17;
then
w = k + 1
by A8, A15, A32, FUNCT_1:def 4;
hence
contradiction
by A31, NAT_1:13;
verum
end;
rng ((SgmX (R,A)) | (k + 1)) =
(rng ((SgmX (R,A)) | k)) \/ (rng <*((SgmX (R,A)) . (k + 1))*>)
by A12, FINSEQ_1:31
.=
(rng ((SgmX (R,A)) | k)) \/ {((SgmX (R,A)) . (k + 1))}
by FINSEQ_1:38
;
then A33:
rng ((SgmX (R,A)) | (k + 1)) = {((SgmX (R,A)) /. (k + 1))} \/ (rng ((SgmX (R,A)) | k))
by A15, PARTFUN1:def 6;
A34:
k + 1
in dom (SgmX (R,(rng ((SgmX (R,A)) | (k + 1)))))
by A14, A28, FINSEQ_3:25;
(SgmX (R,(rng ((SgmX (R,A)) | (k + 1))))) /. (k + 1) = (SgmX (R,A)) /. (k + 1)
by A28, A20, A19, A13, PRE_POLY:21;
then A35:
for
i being
Element of
NAT st 1
<= i &
i <= (k + 1) - 1 holds
(SgmX (R,(rng ((SgmX (R,A)) | k)))) /. i = (SgmX (R,(rng ((SgmX (R,A)) | (k + 1))))) /. i
by A13, A29, A33, A34, PRE_POLY:78;
A36:
i in NAT
by ORDINAL1:def 12;
per cases
( i < k + 1 or i = k + 1 )
by A7, XXREAL_0:1;
suppose
i < k + 1
;
(SgmX (R,(rng ((SgmX (R,A)) | (k + 1))))) /. i = (SgmX (R,A)) /. ithen A37:
i <= k
by NAT_1:13;
hence (SgmX (R,(rng ((SgmX (R,A)) | (k + 1))))) /. i =
(SgmX (R,(rng ((SgmX (R,A)) | k)))) /. i
by A36, A7, A35
.=
(SgmX (R,A)) /. i
by A11, A6, A37, A7, A2
;
verum end;
end;
for k being Nat holds S1[k]
from NAT_1:sch 2(A4, A5);
hence
for i, k being Nat st 1 <= i & i <= k & k <= card A holds
(SgmX (R,(rng ((SgmX (R,A)) | k)))) /. i = (SgmX (R,A)) /. i
; verum