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 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 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 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 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:32, RFUNCT_3:33;
A2: ( len (CHI (B,C)) = len 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 B . 1 implies (Rland (F,B)) . c = (FinS (F,D)) . 1 ) & ( for n being 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 Th11;
thus ( c in B . 1 implies (Rland (F,B)) . c = (FinS (F,D)) . 1 ) :: thesis: for n being 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, Th13
.= (FinS (F,D)) . 1 by A4, A2, Th4, RFINSEQ:16 ;
:: thesis: verum

end;

let n be 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, Th13;
hence (Rland (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