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 A . 1 implies (Rland F,A) . c = (FinS F,D) . 1 ) & ( for n being Element of NAT st 1 <= n & n < len A & c in (A . (n + 1)) \ (A . n) holds
(Rland 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 A . 1 implies (Rland F,A) . c = (FinS F,D) . 1 ) & ( for n being Element of NAT st 1 <= n & n < len A & c in (A . (n + 1)) \ (A . n) holds
(Rland 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 A . 1 implies (Rland F,A) . c = (FinS F,D) . 1 ) & ( for n being Element of NAT st 1 <= n & n < len A & c in (A . (n + 1)) \ (A . n) holds
(Rland 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 B . 1 implies (Rland F,B) . c = (FinS F,D) . 1 ) & ( for n being Element of NAT st 1 <= n & n < len B & c in (B . (n + 1)) \ (B . n) holds
(Rland F,B) . c = (FinS F,D) . (n + 1) ) ) )
set fd = FinS F,D;
set mf = MIM (FinS F,D);
set h = CHI B,C;
A1: (Rland F,B) . c = Sum (((MIM (FinS F,D)) (#) (CHI B,C)) # c) by RFUNCT_3:35, RFUNCT_3:36;
A2: ( len (CHI B,C) = len B & len (MIM (FinS F,D)) = len (FinS F,D) ) by RFINSEQ:def 3, RFUNCT_3:def 6;
assume A3: ( F is total & card C = card D ) ; :: thesis: ( ( c in B . 1 implies (Rland F,B) . c = (FinS F,D) . 1 ) & ( for n being Element of NAT st 1 <= n & n < len B & c in (B . (n + 1)) \ (B . n) holds
(Rland F,B) . c = (FinS F,D) . (n + 1) ) )
then A4: len (MIM (FinS F,D)) = len (CHI B,C) by Th12;
thus ( c in B . 1 implies (Rland F,B) . c = (FinS F,D) . 1 ) :: thesis: for n being Element of NAT st 1 <= n & n < len B & c in (B . (n + 1)) \ (B . n) holds
(Rland F,B) . c = (FinS F,D) . (n + 1)

proof

assume c in B . 1 ; :: thesis: (Rland F,B) . c = (FinS F,D) . 1
hence (Rland F,B) . c = Sum (MIM (FinS F,D)) by A3, A1, Th14
.= (FinS F,D) . 1 by A4, A2, Th4, RFINSEQ:29 ;
:: thesis: verum

end;

let n be Element of NAT ; :: thesis: ( 1 <= n & n < len B & c in (B . (n + 1)) \ (B . n) implies (Rland F,B) . c = (FinS F,D) . (n + 1) )
set mfn = MIM ((FinS F,D) /^ n);
assume that
A5: 1 <= n and
A6: n < len B and
A7: c in (B . (n + 1)) \ (B . n) ; :: thesis: (Rland F,B) . c = (FinS F,D) . (n + 1)
((MIM (FinS F,D)) (#) (CHI B,C)) # c = (n |-> 0 ) ^ (MIM ((FinS F,D) /^ n)) by A3, A5, A6, A7, Th14;
hence (Rland F,B) . c = (Sum (n |-> 0 )) + (Sum (MIM ((FinS F,D) /^ n))) by A1, RVSUM_1:105
.= 0 + (Sum (MIM ((FinS F,D) /^ n))) by RVSUM_1:111
.= (FinS F,D) . (n + 1) by A4, A2, A6, RFINSEQ:30 ;
:: thesis: verum