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