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 Element of 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 Element of 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 Element of 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 Element of 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;
assume A1: ( 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 Element of 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) ) )
A2: (Rlor F,B) . c = Sum (((MIM (FinS F,D)) (#) (CHI (Co_Gen B),C)) # c) by RFUNCT_3:35, RFUNCT_3:36;
A3: ( len (MIM (FinS F,D)) = len (CHI (Co_Gen B),C) & len (CHI (Co_Gen B),C) = len (Co_Gen B) & len (MIM (FinS F,D)) = len (FinS F,D) ) by A1, Th12, RFINSEQ:def 3, RFUNCT_3:def 6;
thus ( c in (Co_Gen B) . 1 implies (Rlor F,B) . c = (FinS F,D) . 1 ) :: thesis: for n being Element of 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 A1, A2, Th14
.= (FinS F,D) . 1 by A3, Th4, RFINSEQ:29 ;
:: thesis: verum

end;

let n be Element of 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 A4: ( 1 <= n & n < len (Co_Gen B) & c in ((Co_Gen B) . (n + 1)) \ ((Co_Gen B) . n) ) ; :: thesis: (Rlor F,B) . c = (FinS F,D) . (n + 1)
then ((MIM (FinS F,D)) (#) (CHI (Co_Gen B),C)) # c = (n |-> 0 ) ^ (MIM ((FinS F,D) /^ n)) by A1, Th14;
hence (Rlor F,B) . c = (Sum (n |-> 0 )) + (Sum (MIM ((FinS F,D) /^ n))) by A2, RVSUM_1:105
.= 0 + (Sum (MIM ((FinS F,D) /^ n))) by RVSUM_1:111
.= (FinS F,D) . (n + 1) by A3, A4, RFINSEQ:30 ;
:: thesis: verum