let C, D be non empty finite set ; :: thesis:
let c be Element of C; :: thesis:
let F be PartFunc of D,REAL ; :: thesis:
let A be RearrangmentGen of C; :: thesis:
assume A1: ( F is total & card C = card D ) ; :: thesis:
set fd = FinS F,D;
set mf = MIM (FinS F,D);
set h = CHI A,C;
set fh = ((MIM (FinS F,D)) (#) (CHI A,C)) # c;
A2: ( dom A = Seg (len A) & dom (MIM (FinS F,D)) = Seg (len (MIM (FinS F,D))) & dom (CHI A,C) = Seg (len (CHI A,C)) & dom ((MIM (FinS F,D)) (#) (CHI A,C)) = Seg (len ((MIM (FinS F,D)) (#) (CHI A,C))) & dom (((MIM (FinS F,D)) (#) (CHI A,C)) # c) = Seg (len (((MIM (FinS F,D)) (#) (CHI A,C)) # c)) ) by FINSEQ_1:def 3;
A3: ( len (MIM (FinS F,D)) = len (CHI A,C) & len (CHI A,C) = len A & len (MIM (FinS F,D)) = len (FinS F,D) & min (len (MIM (FinS F,D))),(len (CHI A,C)) = len ((MIM (FinS F,D)) (#) (CHI A,C)) & len (((MIM (FinS F,D)) (#) (CHI A,C)) # c) = len ((MIM (FinS F,D)) (#) (CHI A,C)) ) by A1, Th12, RFINSEQ:def 3, RFUNCT_3:def 6, RFUNCT_3:def 7, RFUNCT_3:def 8;
thus ( c in A . 1 implies ((MIM (FinS F,D)) (#) (CHI A,C)) # c = MIM (FinS F,D) ) :: thesis:

proof

assume A4: c in A . 1 ; :: thesis:
A5: for n being Element of NAT st n in dom A holds
c in A . n

proof

let n be Element of NAT ; :: thesis:
assume A6: n in dom A ; :: thesis:
then A7: ( 1 <= n & n <= len A ) by FINSEQ_3:27;
then 1 <= len A by XXREAL_0:2;
then 1 in dom A by FINSEQ_3:27;
then A . 1 c= A . n by A6, A7, Th2;
hence c in A . n by A4; :: thesis:

end;

X: dom (((MIM (FinS F,D)) (#) (CHI A,C)) # c) = Seg (len (MIM (FinS F,D))) by A3, FINSEQ_1:def 3;

now

let m be Nat; :: thesis:
assume A8: m in dom (((MIM (FinS F,D)) (#) (CHI A,C)) # c) ; :: thesis:
then A9: m in dom (MIM (FinS F,D)) by X, FINSEQ_1:def 3;
reconsider m1 = m as Element of NAT by ORDINAL1:def 13;
A10: (CHI A,C) . m = chi (A . m),C by A2, A3, A8, RFUNCT_3:def 6;
A11: ( 1 <= m & m <= len (MIM (FinS F,D)) ) by A9, FINSEQ_3:27;
A12: c in A . m by A2, A3, A5, A8;
reconsider r1 = (FinS F,D) . m as Real ;

now

per cases ;

case A13: m = len (MIM (FinS F,D)) ; :: thesis:

then (MIM (FinS F,D)) . m = r1 by A3, RFINSEQ:def 3;
then ((MIM (FinS F,D)) (#) (CHI A,C)) . m = r1 (#) (chi (A . m),C) by A2, A3, A8, A10, RFUNCT_3:def 7;
then A14: (((MIM (FinS F,D)) (#) (CHI A,C)) # c) . m = (r1 (#) (chi (A . m),C)) . c by A8, RFUNCT_3:def 8;
dom (r1 (#) (chi (A . m),C)) = dom (chi (A . m),C) by VALUED_1:def 5
.= C by RFUNCT_1:77 ;
hence (((MIM (FinS F,D)) (#) (CHI A,C)) # c) . m = r1 * ((chi (A . m),C) . c) by A14, VALUED_1:def 5
.= r1 * 1 by A12, RFUNCT_1:79
.= (MIM (FinS F,D)) . m by A3, A13, RFINSEQ:def 3 ;
:: thesis:

end;

case m <> len (MIM (FinS F,D)) ; :: thesis:

then m < len (MIM (FinS F,D)) by A11, XXREAL_0:1;
then ( m + 1 <= len (MIM (FinS F,D)) & m <= m + 1 ) by NAT_1:13;
then A15: ( m <= (len (MIM (FinS F,D))) - 1 & 1 <= m + 1 ) by A11, XREAL_1:21, XXREAL_0:2;
reconsider r2 = (FinS F,D) . (m + 1) as Real ;
(MIM (FinS F,D)) . m1 = r1 - r2 by A11, A15, RFINSEQ:def 3;
then ((MIM (FinS F,D)) (#) (CHI A,C)) . m = (r1 - r2) (#) (chi (A . m),C) by A2, A3, A8, A10, RFUNCT_3:def 7;
then A16: (((MIM (FinS F,D)) (#) (CHI A,C)) # c) . m = ((r1 - r2) (#) (chi (A . m),C)) . c by A8, RFUNCT_3:def 8;
dom ((r1 - r2) (#) (chi (A . m),C)) = dom (chi (A . m),C) by VALUED_1:def 5
.= C by RFUNCT_1:77 ;
hence (((MIM (FinS F,D)) (#) (CHI A,C)) # c) . m = (r1 - r2) * ((chi (A . m),C) . c) by A16, VALUED_1:def 5
.= (r1 - r2) * 1 by A12, RFUNCT_1:79
.= (MIM (FinS F,D)) . m1 by A11, A15, RFINSEQ:def 3 ;
:: thesis:

end;

hence (((MIM (FinS F,D)) (#) (CHI A,C)) # c) . m = (MIM (FinS F,D)) . m ; :: thesis:

end;

hence ((MIM (FinS F,D)) (#) (CHI A,C)) # c = MIM (FinS F,D) by A3, FINSEQ_2:10; :: thesis:

end;

let n be Element of NAT ; :: thesis:
set fdn = (FinS F,D) /^ n;
set mfn = MIM ((FinS F,D) /^ n);
set n0 = n |-> 0 ;
assume A17: ( 1 <= n & n < len A & c in (A . (n + 1)) \ (A . n) ) ; :: thesis:
then A18: ( n <= len A & n + 1 <= len A & n <= n + 1 ) by NAT_1:13;
A19: ( len ((FinS F,D) /^ n) = (len (FinS F,D)) - n & len (MIM ((FinS F,D) /^ n)) = len ((FinS F,D) /^ n) & len (n |-> 0 ) = n & 1 <= n + 1 & len ((MIM (FinS F,D)) /^ n) = (len (MIM (FinS F,D))) - n ) by A3, A17, FINSEQ_1:def 18, NAT_1:13, RFINSEQ:def 2, RFINSEQ:def 3;
A20: ( dom ((FinS F,D) /^ n) = Seg (len ((FinS F,D) /^ n)) & dom (MIM ((FinS F,D) /^ n)) = Seg (len (MIM ((FinS F,D) /^ n))) & dom (n |-> 0 ) = Seg (len (n |-> 0 )) & dom ((MIM (FinS F,D)) /^ n) = Seg (len ((MIM (FinS F,D)) /^ n)) ) by FINSEQ_1:def 3;
A21: len ((n |-> 0 ) ^ (MIM ((FinS F,D) /^ n))) = n + ((len (FinS F,D)) - n) by A19, FINSEQ_1:35
.= len (MIM (FinS F,D)) by RFINSEQ:def 3 ;
A22: ( c in A . (n + 1) & not c in A . n ) by A17, XBOOLE_0:def 5;
A23: for k being Element of NAT st k in dom A & n + 1 <= k holds
c in A . k

proof

let k be Element of NAT ; :: thesis:
assume A24: ( k in dom A & n + 1 <= k ) ; :: thesis:
n + 1 in dom A by A18, A19, FINSEQ_3:27;
then A . (n + 1) c= A . k by A24, Th2;
hence c in A . k by A22; :: thesis:

end;

A25: for k being Element of NAT st k in dom A & k <= n holds
not c in A . k

proof

let k be Element of NAT ; :: thesis:
assume A26: ( k in dom A & k <= n ) ; :: thesis:
n in dom A by A17, FINSEQ_3:27;
then A27: A . k c= A . n by A26, Th2;
assume c in A . k ; :: thesis:
hence contradiction by A17, A27, XBOOLE_0:def 5; :: thesis:

end;

X: dom ((n |-> 0 ) ^ (MIM ((FinS F,D) /^ n))) = Seg (len (MIM (FinS F,D))) by A21, FINSEQ_1:def 3;

now

let m be Nat; :: thesis:
assume A28: m in dom ((n |-> 0 ) ^ (MIM ((FinS F,D) /^ n))) ; :: thesis:
then A29: m in dom (MIM (FinS F,D)) by X, FINSEQ_1:def 3;
reconsider m1 = m as Element of NAT by ORDINAL1:def 13;
A30: (CHI A,C) . m = chi (A . m),C by A2, A3, A28, X, RFUNCT_3:def 6;
A31: ( 1 <= m & m <= len (MIM (FinS F,D)) & m <= m + 1 ) by A29, FINSEQ_3:27, NAT_1:11;
reconsider r1 = (FinS F,D) . m as Real ;

now

per cases ;

case A32: m <= n ; :: thesis:

then not c in A . m by A2, A3, A25, A28, X;
then A33: (chi (A . m),C) . c = 0 by RFUNCT_1:80;
A34: m in Seg n by A31, A32, FINSEQ_1:3;
then A35: (n |-> 0 ) . m = 0 by FUNCOP_1:13;
m < n + 1 by A32, NAT_1:13;
then m < len A by A18, XXREAL_0:2;
then m + 1 <= len A by NAT_1:13;
then A36: m <= (len (MIM (FinS F,D))) - 1 by A3, XREAL_1:21;
reconsider r2 = (FinS F,D) . (m + 1) as Real ;
(MIM (FinS F,D)) . m1 = r1 - r2 by A31, A36, RFINSEQ:def 3;
then ((MIM (FinS F,D)) (#) (CHI A,C)) . m = (r1 - r2) (#) (chi (A . m),C) by A2, A3, A28, A30, X, RFUNCT_3:def 7;
then A37: (((MIM (FinS F,D)) (#) (CHI A,C)) # c) . m = ((r1 - r2) (#) (chi (A . m),C)) . c by A2, A3, A28, X, RFUNCT_3:def 8;
dom ((r1 - r2) (#) (chi (A . m),C)) = dom (chi (A . m),C) by VALUED_1:def 5
.= C by RFUNCT_1:77 ;
hence (((MIM (FinS F,D)) (#) (CHI A,C)) # c) . m = (r1 - r2) * ((chi (A . m),C) . c) by A37, VALUED_1:def 5
.= ((n |-> 0 ) ^ (MIM ((FinS F,D) /^ n))) . m by A19, A20, A33, A34, A35, FINSEQ_1:def 7 ;
:: thesis:

end;

case A38: n < m ; :: thesis:

then A39: ( n + 1 <= m & n <= m ) by NAT_1:13;
then c in A . m by A2, A3, A23, A28, X;
then A40: (chi (A . m),C) . c = 1 by RFUNCT_1:79;
max 0 ,(m - n) = m - n by A38, FINSEQ_2:4;
then reconsider mn = m - n as Element of NAT by FINSEQ_2:5;
A41: 1 <= mn by A39, XREAL_1:21;

now

per cases ;

case A42: m = len (MIM (FinS F,D)) ; :: thesis:

then (MIM (FinS F,D)) . m = r1 by A3, RFINSEQ:def 3;
then ((MIM (FinS F,D)) (#) (CHI A,C)) . m = r1 (#) (chi (A . m),C) by A2, A3, A28, A30, X, RFUNCT_3:def 7;
then A43: (((MIM (FinS F,D)) (#) (CHI A,C)) # c) . m = (r1 (#) (chi (A . m),C)) . c by A2, A3, A28, X, RFUNCT_3:def 8;
A44: mn in dom ((MIM (FinS F,D)) /^ n) by A19, A41, A42, FINSEQ_3:27;
A45: ((n |-> 0 ) ^ (MIM ((FinS F,D) /^ n))) . m = (MIM ((FinS F,D) /^ n)) . (m - n) by A19, A21, A31, A38, FINSEQ_1:37
.= ((MIM (FinS F,D)) /^ n) . mn by RFINSEQ:28
.= (MIM (FinS F,D)) . (mn + n) by A3, A17, A44, RFINSEQ:def 2
.= r1 by A3, A42, RFINSEQ:def 3 ;
dom (r1 (#) (chi (A . m),C)) = dom (chi (A . m),C) by VALUED_1:def 5
.= C by RFUNCT_1:77 ;
hence (((MIM (FinS F,D)) (#) (CHI A,C)) # c) . m = r1 * ((chi (A . m),C) . c) by A43, VALUED_1:def 5
.= ((n |-> 0 ) ^ (MIM ((FinS F,D) /^ n))) . m by A40, A45 ;
:: thesis:

end;

case m <> len (MIM (FinS F,D)) ; :: thesis:

then m < len (MIM (FinS F,D)) by A31, XXREAL_0:1;
then ( m + 1 <= len (MIM (FinS F,D)) & m <= m + 1 ) by NAT_1:13;
then A46: ( m <= (len (MIM (FinS F,D))) - 1 & 1 <= m + 1 ) by NAT_1:11, XREAL_1:21;
reconsider r2 = (FinS F,D) . (m + 1) as Real ;
(MIM (FinS F,D)) . m1 = r1 - r2 by A31, A46, RFINSEQ:def 3;
then ((MIM (FinS F,D)) (#) (CHI A,C)) . m = (r1 - r2) (#) (chi (A . m),C) by A2, A3, A28, A30, X, RFUNCT_3:def 7;
then A47: (((MIM (FinS F,D)) (#) (CHI A,C)) # c) . m = ((r1 - r2) (#) (chi (A . m),C)) . c by A2, A3, A28, X, RFUNCT_3:def 8;
mn <= len ((MIM (FinS F,D)) /^ n) by A19, A31, XREAL_1:11;
then A48: mn in dom ((MIM (FinS F,D)) /^ n) by A41, FINSEQ_3:27;
A49: ((n |-> 0 ) ^ (MIM ((FinS F,D) /^ n))) . m = (MIM ((FinS F,D) /^ n)) . (m - n) by A19, A21, A31, A38, FINSEQ_1:37
.= ((MIM (FinS F,D)) /^ n) . mn by RFINSEQ:28
.= (MIM (FinS F,D)) . (mn + n) by A3, A17, A48, RFINSEQ:def 2
.= r1 - r2 by A31, A46, RFINSEQ:def 3 ;
dom ((r1 - r2) (#) (chi (A . m),C)) = dom (chi (A . m),C) by VALUED_1:def 5
.= C by RFUNCT_1:77 ;
hence (((MIM (FinS F,D)) (#) (CHI A,C)) # c) . m = (r1 - r2) * ((chi (A . m),C) . c) by A47, VALUED_1:def 5
.= ((n |-> 0 ) ^ (MIM ((FinS F,D) /^ n))) . m by A40, A49 ;
:: thesis:

end;

hence (((MIM (FinS F,D)) (#) (CHI A,C)) # c) . m = ((n |-> 0 ) ^ (MIM ((FinS F,D) /^ n))) . m ; :: thesis:

end;

hence (((MIM (FinS F,D)) (#) (CHI A,C)) # c) . m = ((n |-> 0 ) ^ (MIM ((FinS F,D) /^ n))) . m ; :: thesis:

end;

hence ((MIM (FinS F,D)) (#) (CHI A,C)) # c = (n |-> 0 ) ^ (MIM ((FinS F,D) /^ n)) by A3, A21, FINSEQ_2:10; :: thesis: