let n be Element of NAT ; for D, C 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 D, C 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, Th31;
defpred S1[ Element of 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 Element of NAT st S1[m] holds
S1[m + 1]
proof
set f =
FinS (Rland F,B),
C;
let m be
Element of
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:27;
then A10:
m + 1
in Seg (m + 1)
by FINSEQ_1:3;
A11:
dom (Rland F,B) = C
by A1, Th13;
A12:
m + 1
<= len B
by A9, FINSEQ_3:27;
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:21;
A16:
len ((FinS (Rland F,B),C) | (m + 1)) = m + 1
by A4, A3, A12, FINSEQ_1:80;
now 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, Th31;
then
( 1
in Seg 1 & 1
in dom (FinS (Rland F,B),C) )
by FINSEQ_1:3, FINSEQ_3:27;
then A21:
((FinS (Rland F,B),C) | (m + 1)) . 1 =
(FinS (Rland F,B),C) . 1
by A17, RFINSEQ:19
.=
(FinS F,D) . 1
by A1, Th18
.=
(Rland F,B) . d
by A1, A19, Th15
;
dom (Rland F,B) = C
by A1, Th13;
then A22:
FinS (Rland F,B),
(B . (m + 1)) = <*((Rland F,B) . d)*>
by A17, A18, RFUNCT_3:72;
len ((FinS (Rland F,B),C) | (m + 1)) = 1
by A17, A20, FINSEQ_1:80;
hence
(FinS (Rland F,B),C) | (m + 1) = FinS (Rland F,B),
(B . (m + 1))
by A22, A21, FINSEQ_1:57;
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:7;
A25:
((FinS (Rland F,B),C) | (m + 1)) | m =
((FinS (Rland F,B),C) | (m + 1)) | (Seg m)
by FINSEQ_1:def 15
.=
((FinS (Rland F,B),C) | (Seg (m + 1))) | (Seg m)
by FINSEQ_1:def 15
.=
(FinS (Rland F,B),C) | ((Seg (m + 1)) /\ (Seg m))
by RELAT_1:100
.=
(FinS (Rland F,B),C) | (Seg m)
by A24, XBOOLE_1:28
.=
(FinS (Rland F,B),C) | m
by FINSEQ_1:def 15
;
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, Th15
.=
(FinS (Rland F,B),C) . (m + 1)
by A1, Th18
.=
((FinS (Rland F,B),C) | (m + 1)) . (m + 1)
by A5, A4, A3, A9, A10, RFINSEQ:19
;
then A30:
(FinS (Rland F,B),C) | (m + 1) = ((FinS (Rland F,B),C) | m) ^ <*((Rland F,B) . d)*>
by A16, A25, RFINSEQ:20;
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:90;
A32:
(FinS (Rland F,B),C) | (m + 1) is
non-increasing
by RFINSEQ:33;
A33:
dom ((Rland F,B) | (B . (m + 1))) =
(dom (Rland F,B)) /\ (B . (m + 1))
by RELAT_1:90
.=
B . (m + 1)
by A9, A11, Lm5, XBOOLE_1:28
;
B . (m + 1) is
finite
by A9, Lm5, FINSET_1:13;
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:27, RFUNCT_3:68;
hence
(FinS (Rland F,B),C) | (m + 1) = FinS (Rland F,B),
(B . (m + 1))
by A33, A32, RFUNCT_3:def 14;
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:27;
for m being Element of NAT holds S1[m]
from NAT_1:sch 1(A34, A6);
hence
(FinS (Rland F,B),C) | n = FinS (Rland F,B),(B . n)
by A2; verum