let n be Nat; for C, D being non empty finite set
for F being PartFunc of D,REAL
for A being RearrangmentGen of C st F is total & card D = card C & n in dom A holds
(FinS ((Rland (F,A)),C)) | n = FinS ((Rland (F,A)),(A . n))
let C, D be non empty finite set ; for F being PartFunc of D,REAL
for A being RearrangmentGen of C st F is total & card D = card C & n in dom A holds
(FinS ((Rland (F,A)),C)) | n = FinS ((Rland (F,A)),(A . n))
let F be PartFunc of D,REAL; for A being RearrangmentGen of C st F is total & card D = card C & n in dom A holds
(FinS ((Rland (F,A)),C)) | n = FinS ((Rland (F,A)),(A . n))
let B be RearrangmentGen of C; ( F is total & card D = card C & n in dom B implies (FinS ((Rland (F,B)),C)) | n = FinS ((Rland (F,B)),(B . n)) )
assume that
A1:
( F is total & card D = card C )
and
A2:
n in dom B
; (FinS ((Rland (F,B)),C)) | n = FinS ((Rland (F,B)),(B . n))
set p = Rland (F,B);
A3:
len (FinS ((Rland (F,B)),C)) = card C
by A1, Th30;
defpred S1[ Nat] means ( $1 in dom B implies (FinS ((Rland (F,B)),C)) | $1 = FinS ((Rland (F,B)),(B . $1)) );
A4:
len B = card C
by Th1;
A5:
( dom B = Seg (len B) & dom (FinS ((Rland (F,B)),C)) = Seg (len (FinS ((Rland (F,B)),C))) )
by FINSEQ_1:def 3;
A6:
for m being Nat st S1[m] holds
S1[m + 1]
proof
set f =
FinS (
(Rland (F,B)),
C);
let m be
Nat;
( S1[m] implies S1[m + 1] )
assume A7:
S1[
m]
;
S1[m + 1]
A8:
m <= m + 1
by NAT_1:11;
assume A9:
m + 1
in dom B
;
(FinS ((Rland (F,B)),C)) | (m + 1) = FinS ((Rland (F,B)),(B . (m + 1)))
then
1
<= m + 1
by FINSEQ_3:25;
then A10:
m + 1
in Seg (m + 1)
by FINSEQ_1:1;
A11:
dom (Rland (F,B)) = C
by A1, Th12;
A12:
m + 1
<= len B
by A9, FINSEQ_3:25;
then A13:
m <= len B
by NAT_1:13;
A14:
m < len B
by A12, NAT_1:13;
A15:
m <= (len B) - 1
by A12, XREAL_1:19;
A16:
len ((FinS ((Rland (F,B)),C)) | (m + 1)) = m + 1
by A4, A3, A12, FINSEQ_1:59;
now ( ( m = 0 & (FinS ((Rland (F,B)),C)) | (m + 1) = FinS ((Rland (F,B)),(B . (m + 1))) ) or ( m <> 0 & (FinS ((Rland (F,B)),C)) | (m + 1) = FinS ((Rland (F,B)),(B . (m + 1))) ) )per cases
( m = 0 or m <> 0 )
;
case A17:
m = 0
;
(FinS ((Rland (F,B)),C)) | (m + 1) = FinS ((Rland (F,B)),(B . (m + 1)))consider d being
Element of
C such that A18:
B . 1
= {d}
by Th9;
A19:
d in B . 1
by A18, TARSKI:def 1;
A20:
1
<= len (FinS ((Rland (F,B)),C))
by A1, Th30;
then
( 1
in Seg 1 & 1
in dom (FinS ((Rland (F,B)),C)) )
by FINSEQ_1:1, FINSEQ_3:25;
then A21:
((FinS ((Rland (F,B)),C)) | (m + 1)) . 1 =
(FinS ((Rland (F,B)),C)) . 1
by A17, RFINSEQ:6
.=
(FinS (F,D)) . 1
by A1, Th17
.=
(Rland (F,B)) . d
by A1, A19, Th14
;
dom (Rland (F,B)) = C
by A1, Th12;
then A22:
FinS (
(Rland (F,B)),
(B . (m + 1)))
= <*((Rland (F,B)) . d)*>
by A17, A18, RFUNCT_3:69;
len ((FinS ((Rland (F,B)),C)) | (m + 1)) = 1
by A17, A20, FINSEQ_1:59;
hence
(FinS ((Rland (F,B)),C)) | (m + 1) = FinS (
(Rland (F,B)),
(B . (m + 1)))
by A22, A21, FINSEQ_1:40;
verum end; case A23:
m <> 0
;
(FinS ((Rland (F,B)),C)) | (m + 1) = FinS ((Rland (F,B)),(B . (m + 1)))A24:
Seg m c= Seg (m + 1)
by A8, FINSEQ_1:5;
A25:
((FinS ((Rland (F,B)),C)) | (m + 1)) | m =
((FinS ((Rland (F,B)),C)) | (m + 1)) | (Seg m)
by FINSEQ_1:def 16
.=
((FinS ((Rland (F,B)),C)) | (Seg (m + 1))) | (Seg m)
by FINSEQ_1:def 16
.=
(FinS ((Rland (F,B)),C)) | ((Seg (m + 1)) /\ (Seg m))
by RELAT_1:71
.=
(FinS ((Rland (F,B)),C)) | (Seg m)
by A24, XBOOLE_1:28
.=
(FinS ((Rland (F,B)),C)) | m
by FINSEQ_1:def 16
;
A26:
0 + 1
<= m
by A23, NAT_1:13;
then consider d being
Element of
C such that A27:
(B . (m + 1)) \ (B . m) = {d}
and
B . (m + 1) = (B . m) \/ {d}
and A28:
(B . (m + 1)) \ {d} = B . m
by A15, Th10;
A29:
d in {d}
by TARSKI:def 1;
then (Rland (F,B)) . d =
(FinS (F,D)) . (m + 1)
by A1, A14, A26, A27, Th14
.=
(FinS ((Rland (F,B)),C)) . (m + 1)
by A1, Th17
.=
((FinS ((Rland (F,B)),C)) | (m + 1)) . (m + 1)
by A5, A4, A3, A9, A10, RFINSEQ:6
;
then A30:
(FinS ((Rland (F,B)),C)) | (m + 1) = ((FinS ((Rland (F,B)),C)) | m) ^ <*((Rland (F,B)) . d)*>
by A16, A25, RFINSEQ:7;
d in (dom (Rland (F,B))) /\ (B . (m + 1))
by A11, A27, A29, XBOOLE_0:def 4;
then A31:
d in dom ((Rland (F,B)) | (B . (m + 1)))
by RELAT_1:61;
A32:
(FinS ((Rland (F,B)),C)) | (m + 1) is
non-increasing
by RFINSEQ:20;
A33:
dom ((Rland (F,B)) | (B . (m + 1))) =
(dom (Rland (F,B))) /\ (B . (m + 1))
by RELAT_1:61
.=
B . (m + 1)
by A9, A11, Lm5, XBOOLE_1:28
;
B . (m + 1) is
finite
by A9, Lm5, FINSET_1:1;
then
(FinS ((Rland (F,B)),C)) | (m + 1),
(Rland (F,B)) | (B . (m + 1)) are_fiberwise_equipotent
by A7, A13, A26, A28, A30, A31, FINSEQ_3:25, RFUNCT_3:65;
hence
(FinS ((Rland (F,B)),C)) | (m + 1) = FinS (
(Rland (F,B)),
(B . (m + 1)))
by A33, A32, RFUNCT_3:def 13;
verum end;
hence
(FinS ((Rland (F,B)),C)) | (m + 1) = FinS (
(Rland (F,B)),
(B . (m + 1)))
;
verum
end;
A34:
S1[ 0 ]
by FINSEQ_3:25;
for m being Nat holds S1[m]
from NAT_1:sch 2(A34, A6);
hence
(FinS ((Rland (F,B)),C)) | n = FinS ((Rland (F,B)),(B . n))
by A2; verum