let C, D be non empty finite set ; for c being Element of C
for F being PartFunc of D,REAL
for A being RearrangmentGen of C st F is total & card C = card D holds
( ( c in (Co_Gen A) . 1 implies (Rlor (F,A)) . c = (FinS (F,D)) . 1 ) & ( for n being Nat st 1 <= n & n < len (Co_Gen A) & c in ((Co_Gen A) . (n + 1)) \ ((Co_Gen A) . n) holds
(Rlor (F,A)) . c = (FinS (F,D)) . (n + 1) ) )
let c be Element of C; for F being PartFunc of D,REAL
for A being RearrangmentGen of C st F is total & card C = card D holds
( ( c in (Co_Gen A) . 1 implies (Rlor (F,A)) . c = (FinS (F,D)) . 1 ) & ( for n being Nat st 1 <= n & n < len (Co_Gen A) & c in ((Co_Gen A) . (n + 1)) \ ((Co_Gen A) . n) holds
(Rlor (F,A)) . c = (FinS (F,D)) . (n + 1) ) )
let F be PartFunc of D,REAL; for A being RearrangmentGen of C st F is total & card C = card D holds
( ( c in (Co_Gen A) . 1 implies (Rlor (F,A)) . c = (FinS (F,D)) . 1 ) & ( for n being Nat st 1 <= n & n < len (Co_Gen A) & c in ((Co_Gen A) . (n + 1)) \ ((Co_Gen A) . n) holds
(Rlor (F,A)) . c = (FinS (F,D)) . (n + 1) ) )
let B be RearrangmentGen of C; ( F is total & card C = card D implies ( ( c in (Co_Gen B) . 1 implies (Rlor (F,B)) . c = (FinS (F,D)) . 1 ) & ( for n being Nat st 1 <= n & n < len (Co_Gen B) & c in ((Co_Gen B) . (n + 1)) \ ((Co_Gen B) . n) holds
(Rlor (F,B)) . c = (FinS (F,D)) . (n + 1) ) ) )
set fd = FinS (F,D);
set mf = MIM (FinS (F,D));
set b = Co_Gen B;
set h = CHI ((Co_Gen B),C);
A1:
(Rlor (F,B)) . c = Sum (((MIM (FinS (F,D))) (#) (CHI ((Co_Gen B),C))) # c)
by RFUNCT_3:32, RFUNCT_3:33;
A2:
( len (CHI ((Co_Gen B),C)) = len (Co_Gen B) & len (MIM (FinS (F,D))) = len (FinS (F,D)) )
by RFINSEQ:def 2, RFUNCT_3:def 6;
assume A3:
( F is total & card C = card D )
; ( ( c in (Co_Gen B) . 1 implies (Rlor (F,B)) . c = (FinS (F,D)) . 1 ) & ( for n being Nat st 1 <= n & n < len (Co_Gen B) & c in ((Co_Gen B) . (n + 1)) \ ((Co_Gen B) . n) holds
(Rlor (F,B)) . c = (FinS (F,D)) . (n + 1) ) )
then A4:
len (MIM (FinS (F,D))) = len (CHI ((Co_Gen B),C))
by Th11;
thus
( c in (Co_Gen B) . 1 implies (Rlor (F,B)) . c = (FinS (F,D)) . 1 )
for n being Nat st 1 <= n & n < len (Co_Gen B) & c in ((Co_Gen B) . (n + 1)) \ ((Co_Gen B) . n) holds
(Rlor (F,B)) . c = (FinS (F,D)) . (n + 1)proof
assume
c in (Co_Gen B) . 1
;
(Rlor (F,B)) . c = (FinS (F,D)) . 1
hence (Rlor (F,B)) . c =
Sum (MIM (FinS (F,D)))
by A3, A1, Th13
.=
(FinS (F,D)) . 1
by A4, A2, Th4, RFINSEQ:16
;
verum
end;
let n be Nat; ( 1 <= n & n < len (Co_Gen B) & c in ((Co_Gen B) . (n + 1)) \ ((Co_Gen B) . n) implies (Rlor (F,B)) . c = (FinS (F,D)) . (n + 1) )
set mfn = MIM ((FinS (F,D)) /^ n);
assume that
A5:
1 <= n
and
A6:
n < len (Co_Gen B)
and
A7:
c in ((Co_Gen B) . (n + 1)) \ ((Co_Gen B) . n)
; (Rlor (F,B)) . c = (FinS (F,D)) . (n + 1)
((MIM (FinS (F,D))) (#) (CHI ((Co_Gen B),C))) # c = (n |-> 0) ^ (MIM ((FinS (F,D)) /^ n))
by A3, A5, A6, A7, Th13;
hence (Rlor (F,B)) . c =
(Sum (n |-> (In (0,REAL)))) + (Sum (MIM ((FinS (F,D)) /^ n)))
by A1, RVSUM_1:75
.=
0 + (Sum (MIM ((FinS (F,D)) /^ n)))
by RVSUM_1:81
.=
(FinS (F,D)) . (n + 1)
by A4, A2, A6, RFINSEQ:17
;
verum