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