let n be Element of NAT ; :: thesis: 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 ; :: thesis: 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 ; :: thesis: 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; :: thesis: ( 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 A1:
( F is total & card D = card C & n in dom B )
; :: thesis: (FinS (Rlor F,B),C) | n = FinS (Rlor F,B),((Co_Gen B) . n)
set p = Rlor F,B;
set b = Co_Gen B;
A2:
( dom B = Seg (len B) & dom (Co_Gen B) = Seg (len (Co_Gen B)) & dom (FinS (Rlor F,B),C) = Seg (len (FinS (Rlor F,B),C)) )
by FINSEQ_1:def 3;
A3:
( len B = card C & len (Co_Gen B) = card C & len (FinS (Rlor F,B),C) = card C )
by A1, Th1, 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:
S1[ 0 ]
by FINSEQ_3:27;
A5:
for m being Element of NAT st S1[m] holds
S1[m + 1]
proof
let m be
Element of
NAT ;
:: thesis: ( S1[m] implies S1[m + 1] )
assume A6:
S1[
m]
;
:: thesis: S1[m + 1]
set f =
FinS (Rlor F,B),
C;
assume A7:
m + 1
in dom (Co_Gen B)
;
:: thesis: (FinS (Rlor F,B),C) | (m + 1) = FinS (Rlor F,B),((Co_Gen B) . (m + 1))
then A8:
( 1
<= m + 1 &
m + 1
<= len (Co_Gen B) &
m <= m + 1 )
by FINSEQ_3:27, NAT_1:11;
then A9:
( 1
<= len (Co_Gen B) &
m <= len (Co_Gen B) &
m <= (len (Co_Gen B)) - 1 &
m < len (Co_Gen B) )
by NAT_1:13, XREAL_1:21, XXREAL_0:2;
then A10:
( 1
in dom (Co_Gen B) &
dom ((FinS (Rlor F,B),C) | (m + 1)) = Seg (len ((FinS (Rlor F,B),C) | (m + 1))) &
m + 1
in Seg (m + 1) )
by A8, FINSEQ_1:3, FINSEQ_1:def 3, FINSEQ_3:27;
A11:
len ((FinS (Rlor F,B),C) | (m + 1)) = m + 1
by A3, A8, FINSEQ_1:80;
A12:
dom (Rlor F,B) = C
by A1, Th21;
now per cases
( m = 0 or m <> 0 )
;
case A13:
m = 0
;
:: thesis: (FinS (Rlor F,B),C) | (m + 1) = FinS (Rlor F,B),((Co_Gen B) . (m + 1))consider d being
Element of
C such that A14:
(Co_Gen B) . 1
= {d}
by Th9;
(
(Co_Gen B) . 1
c= C &
dom (Rlor F,B) = C )
by A1, A10, Lm5, Th21;
then A15:
FinS (Rlor F,B),
((Co_Gen B) . (m + 1)) = <*((Rlor F,B) . d)*>
by A13, A14, RFUNCT_3:72;
A16:
d in (Co_Gen B) . 1
by A14, TARSKI:def 1;
A17:
( 1
in Seg 1 & 1
<= len (FinS (Rlor F,B),C) )
by A1, Th36, FINSEQ_1:3;
then A18:
( 1
in dom (FinS (Rlor F,B),C) &
len ((FinS (Rlor F,B),C) | (m + 1)) = 1 )
by A13, FINSEQ_1:80, FINSEQ_3:27;
then ((FinS (Rlor F,B),C) | (m + 1)) . 1 =
(FinS (Rlor F,B),C) . 1
by A13, A17, RFINSEQ:19
.=
(FinS F,D) . 1
by A1, Th25
.=
(Rlor F,B) . d
by A1, A16, Th22
;
hence
(FinS (Rlor F,B),C) | (m + 1) = FinS (Rlor F,B),
((Co_Gen B) . (m + 1))
by A15, A18, FINSEQ_1:57;
:: thesis: verum end; case
m <> 0
;
:: thesis: (FinS (Rlor F,B),C) | (m + 1) = FinS (Rlor F,B),((Co_Gen B) . (m + 1))then
0 < m
;
then A19:
0 + 1
<= m
by NAT_1:13;
then consider d being
Element of
C such that A20:
(
((Co_Gen B) . (m + 1)) \ ((Co_Gen B) . m) = {d} &
(Co_Gen B) . (m + 1) = ((Co_Gen B) . m) \/ {d} &
((Co_Gen B) . (m + 1)) \ {d} = (Co_Gen B) . m )
by A9, Th10;
A21:
Seg m c= Seg (m + 1)
by A8, FINSEQ_1:7;
A22:
((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 A21, XBOOLE_1:28
.=
(FinS (Rlor F,B),C) | m
by FINSEQ_1:def 15
;
A23:
d in {d}
by TARSKI:def 1;
then (Rlor F,B) . d =
(FinS F,D) . (m + 1)
by A1, A9, A19, A20, Th22
.=
(FinS (Rlor F,B),C) . (m + 1)
by A1, Th25
.=
((FinS (Rlor F,B),C) | (m + 1)) . (m + 1)
by A2, A3, A7, A10, RFINSEQ:19
;
then A24:
(FinS (Rlor F,B),C) | (m + 1) = ((FinS (Rlor F,B),C) | m) ^ <*((Rlor F,B) . d)*>
by A11, A22, RFINSEQ:20;
A25:
(Co_Gen B) . (m + 1) is
finite
by A7, Lm5, FINSET_1:13;
d in (dom (Rlor F,B)) /\ ((Co_Gen B) . (m + 1))
by A12, A20, A23, XBOOLE_0:def 4;
then
d in dom ((Rlor F,B) | ((Co_Gen B) . (m + 1)))
by RELAT_1:90;
then A26:
(FinS (Rlor F,B),C) | (m + 1),
(Rlor F,B) | ((Co_Gen B) . (m + 1)) are_fiberwise_equipotent
by A6, A9, A19, A20, A24, A25, FINSEQ_3:27, RFUNCT_3:68;
A27:
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 A7, A12, Lm5, XBOOLE_1:28
;
(FinS (Rlor F,B),C) | (m + 1) is
non-increasing
by RFINSEQ:33;
hence
(FinS (Rlor F,B),C) | (m + 1) = FinS (Rlor F,B),
((Co_Gen B) . (m + 1))
by A26, A27, RFUNCT_3:def 14;
:: thesis: verum end;
hence
(FinS (Rlor F,B),C) | (m + 1) = FinS (Rlor F,B),
((Co_Gen B) . (m + 1))
;
:: thesis: verum
end;
for m being Element of NAT holds S1[m]
from NAT_1:sch 1(A4, A5);
hence
(FinS (Rlor F,B),C) | n = FinS (Rlor F,B),((Co_Gen B) . n)
by A1, A2, A3; :: thesis: verum