let C, D be non empty finite set ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ) ; :: thesis: ( ( 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 ) :: thesis: 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 ; :: thesis: (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 ;
:: thesis: verum

end;

let n be Nat; :: thesis: ( 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) ; :: thesis: (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 ;
:: thesis: verum