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 ((MIM (FinS (F,D))) (#) (CHI (A,C))) # c = MIM (FinS (F,D)) ) & ( for n being Nat st 1 <= n & n < len A & c in (A . (n + 1)) \ (A . n) holds
((MIM (FinS (F,D))) (#) (CHI (A,C))) # c = (n |-> 0) ^ (MIM ((FinS (F,D)) /^ n)) ) )
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 ((MIM (FinS (F,D))) (#) (CHI (A,C))) # c = MIM (FinS (F,D)) ) & ( for n being Nat st 1 <= n & n < len A & c in (A . (n + 1)) \ (A . n) holds
((MIM (FinS (F,D))) (#) (CHI (A,C))) # c = (n |-> 0) ^ (MIM ((FinS (F,D)) /^ n)) ) )
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 ((MIM (FinS (F,D))) (#) (CHI (A,C))) # c = MIM (FinS (F,D)) ) & ( for n being Nat st 1 <= n & n < len A & c in (A . (n + 1)) \ (A . n) holds
((MIM (FinS (F,D))) (#) (CHI (A,C))) # c = (n |-> 0) ^ (MIM ((FinS (F,D)) /^ n)) ) )
let A be RearrangmentGen of C; :: thesis: ( F is total & card C = card D implies ( ( c in A . 1 implies ((MIM (FinS (F,D))) (#) (CHI (A,C))) # c = MIM (FinS (F,D)) ) & ( for n being Nat st 1 <= n & n < len A & c in (A . (n + 1)) \ (A . n) holds
((MIM (FinS (F,D))) (#) (CHI (A,C))) # c = (n |-> 0) ^ (MIM ((FinS (F,D)) /^ n)) ) ) )
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;
A1: dom A = Seg (len A) by FINSEQ_1:def 3;
A2: dom ((MIM (FinS (F,D))) (#) (CHI (A,C))) = Seg (len ((MIM (FinS (F,D))) (#) (CHI (A,C)))) by FINSEQ_1:def 3;
A3: len (CHI (A,C)) = len A by RFUNCT_3:def 6;
A4: len (MIM (FinS (F,D))) = len (FinS (F,D)) by RFINSEQ:def 2;
A5: dom (((MIM (FinS (F,D))) (#) (CHI (A,C))) # c) = Seg (len (((MIM (FinS (F,D))) (#) (CHI (A,C))) # c)) by FINSEQ_1:def 3;
A6: min ((len (MIM (FinS (F,D)))),(len (CHI (A,C)))) = len ((MIM (FinS (F,D))) (#) (CHI (A,C))) by RFUNCT_3:def 7;
assume ( F is total & card C = card D ) ; :: thesis: ( ( c in A . 1 implies ((MIM (FinS (F,D))) (#) (CHI (A,C))) # c = MIM (FinS (F,D)) ) & ( for n being Nat st 1 <= n & n < len A & c in (A . (n + 1)) \ (A . n) holds
((MIM (FinS (F,D))) (#) (CHI (A,C))) # c = (n |-> 0) ^ (MIM ((FinS (F,D)) /^ n)) ) )
then A7: len (MIM (FinS (F,D))) = len (CHI (A,C)) by Th11;
A8: len (((MIM (FinS (F,D))) (#) (CHI (A,C))) # c) = len ((MIM (FinS (F,D))) (#) (CHI (A,C))) by RFUNCT_3:def 8;
A9: dom (CHI (A,C)) = Seg (len (CHI (A,C))) by FINSEQ_1:def 3;
thus ( c in A . 1 implies ((MIM (FinS (F,D))) (#) (CHI (A,C))) # c = MIM (FinS (F,D)) ) :: thesis: for n being Nat st 1 <= n & n < len A & c in (A . (n + 1)) \ (A . n) holds
((MIM (FinS (F,D))) (#) (CHI (A,C))) # c = (n |-> 0) ^ (MIM ((FinS (F,D)) /^ n))

proof

assume A10: c in A . 1 ; :: thesis: ((MIM (FinS (F,D))) (#) (CHI (A,C))) # c = MIM (FinS (F,D))
A11: for n being Nat st n in dom A holds
c in A . n

proof

let n be Nat; :: thesis: ( n in dom A implies c in A . n )
assume A12: n in dom A ; :: thesis: c in A . n
then A13: 1 <= n by FINSEQ_3:25;
n <= len A by A12, FINSEQ_3:25;
then 1 <= len A by A13, XXREAL_0:2;
then 1 in dom A by FINSEQ_3:25;
then A . 1 c= A . n by A12, A13, Th2;
hence c in A . n by A10; :: thesis: verum

end;

A14: dom (((MIM (FinS (F,D))) (#) (CHI (A,C))) # c) = Seg (len (MIM (FinS (F,D)))) by A7, A6, A8, FINSEQ_1:def 3;

now :: thesis: for m being Nat st m in dom (((MIM (FinS (F,D))) (#) (CHI (A,C))) # c) holds
(((MIM (FinS (F,D))) (#) (CHI (A,C))) # c) . m = (MIM (FinS (F,D))) . m

let m be Nat; :: thesis: ( m in dom (((MIM (FinS (F,D))) (#) (CHI (A,C))) # c) implies (((MIM (FinS (F,D))) (#) (CHI (A,C))) # c) . m = (MIM (FinS (F,D))) . m )
reconsider m1 = m as Element of NAT by ORDINAL1:def 12;
reconsider r1 = (FinS (F,D)) . m as Real ;
assume A15: m in dom (((MIM (FinS (F,D))) (#) (CHI (A,C))) # c) ; :: thesis: (((MIM (FinS (F,D))) (#) (CHI (A,C))) # c) . m = (MIM (FinS (F,D))) . m
then A16: 1 <= m by FINSEQ_3:25;
A17: (CHI (A,C)) . m = chi ((A . m),C) by A9, A5, A7, A6, A8, A15, RFUNCT_3:def 6;
A18: c in A . m by A1, A5, A7, A3, A6, A8, A11, A15;
m in dom (MIM (FinS (F,D))) by A14, A15, FINSEQ_1:def 3;
then A19: m <= len (MIM (FinS (F,D))) by FINSEQ_3:25;

now :: thesis: ( ( m = len (MIM (FinS (F,D))) & (((MIM (FinS (F,D))) (#) (CHI (A,C))) # c) . m = (MIM (FinS (F,D))) . m ) or ( m <> len (MIM (FinS (F,D))) & (((MIM (FinS (F,D))) (#) (CHI (A,C))) # c) . m = (MIM (FinS (F,D))) . m1 ) )

per cases ( m = len (MIM (FinS (F,D))) or m <> len (MIM (FinS (F,D))) ) ;

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

then (MIM (FinS (F,D))) . m = r1 by A4, RFINSEQ:def 2;
then ((MIM (FinS (F,D))) (#) (CHI (A,C))) . m = r1 (#) (chi ((A . m),C)) by A2, A5, A8, A15, A17, RFUNCT_3:def 7;
then A21: (((MIM (FinS (F,D))) (#) (CHI (A,C))) # c) . m = (r1 (#) (chi ((A . m),C))) . c by A15, RFUNCT_3:def 8;
dom (r1 (#) (chi ((A . m),C))) = dom (chi ((A . m),C)) by VALUED_1:def 5
.= C by RFUNCT_1:61 ;
hence (((MIM (FinS (F,D))) (#) (CHI (A,C))) # c) . m = r1 * ((chi ((A . m),C)) . c) by A21, VALUED_1:def 5
.= r1 * 1 by A18, RFUNCT_1:63
.= (MIM (FinS (F,D))) . m by A4, A20, RFINSEQ:def 2 ;
:: thesis: verum

end;

case A22: m <> len (MIM (FinS (F,D))) ; :: thesis: (((MIM (FinS (F,D))) (#) (CHI (A,C))) # c) . m = (MIM (FinS (F,D))) . m1

reconsider r2 = (FinS (F,D)) . (m + 1) as Real ;
m < len (MIM (FinS (F,D))) by A19, A22, XXREAL_0:1;
then m + 1 <= len (MIM (FinS (F,D))) by NAT_1:13;
then A23: m <= (len (MIM (FinS (F,D)))) - 1 by XREAL_1:19;
then (MIM (FinS (F,D))) . m1 = r1 - r2 by A16, RFINSEQ:def 2;
then ((MIM (FinS (F,D))) (#) (CHI (A,C))) . m = (r1 - r2) (#) (chi ((A . m),C)) by A2, A5, A8, A15, A17, RFUNCT_3:def 7;
then A24: (((MIM (FinS (F,D))) (#) (CHI (A,C))) # c) . m = ((r1 - r2) (#) (chi ((A . m),C))) . c by A15, 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:61 ;
hence (((MIM (FinS (F,D))) (#) (CHI (A,C))) # c) . m = (r1 - r2) * ((chi ((A . m),C)) . c) by A24, VALUED_1:def 5
.= (r1 - r2) * 1 by A18, RFUNCT_1:63
.= (MIM (FinS (F,D))) . m1 by A16, A23, RFINSEQ:def 2 ;
:: thesis: verum

end;

end;

end;

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

end;

hence ((MIM (FinS (F,D))) (#) (CHI (A,C))) # c = MIM (FinS (F,D)) by A7, A6, A8, FINSEQ_2:9; :: thesis: verum

end;

let n be Nat; :: thesis: ( 1 <= n & n < len A & c in (A . (n + 1)) \ (A . n) implies ((MIM (FinS (F,D))) (#) (CHI (A,C))) # c = (n |-> 0) ^ (MIM ((FinS (F,D)) /^ n)) )
assume that
A25: 1 <= n and
A26: n < len A and
A27: c in (A . (n + 1)) \ (A . n) ; :: thesis: ((MIM (FinS (F,D))) (#) (CHI (A,C))) # c = (n |-> 0) ^ (MIM ((FinS (F,D)) /^ n))
A28: len ((MIM (FinS (F,D))) /^ n) = (len (MIM (FinS (F,D)))) - n by A7, A3, A26, RFINSEQ:def 1;
A29: for k being Nat st k in dom A & k <= n holds
not c in A . k

proof

let k be Nat; :: thesis: ( k in dom A & k <= n implies not c in A . k )
assume A30: ( k in dom A & k <= n ) ; :: thesis: not c in A . k
assume A31: c in A . k ; :: thesis: contradiction
n in dom A by A25, A26, FINSEQ_3:25;
then A . k c= A . n by A30, Th2;
hence contradiction by A27, A31, XBOOLE_0:def 5; :: thesis: verum

end;

A32: c in A . (n + 1) by A27;
A33: n + 1 <= len A by A26, NAT_1:13;
A34: 1 <= n + 1 by A25, NAT_1:13;
A35: for k being Nat st k in dom A & n + 1 <= k holds
c in A . k

proof

let k be Nat; :: thesis: ( k in dom A & n + 1 <= k implies c in A . k )
assume A36: ( k in dom A & n + 1 <= k ) ; :: thesis: c in A . k
n + 1 in dom A by A33, A34, FINSEQ_3:25;
then A . (n + 1) c= A . k by A36, Th2;
hence c in A . k by A32; :: thesis: verum

end;

set fdn = (FinS (F,D)) /^ n;
set mfn = MIM ((FinS (F,D)) /^ n);
set n0 = n |-> 0;
A37: len (MIM ((FinS (F,D)) /^ n)) = len ((FinS (F,D)) /^ n) by RFINSEQ:def 2;
A38: len (n |-> 0) = n by CARD_1:def 7;
len ((FinS (F,D)) /^ n) = (len (FinS (F,D))) - n by A7, A3, A4, A26, RFINSEQ:def 1;
then A39: len ((n |-> 0) ^ (MIM ((FinS (F,D)) /^ n))) = n + ((len (FinS (F,D))) - n) by A37, A38, FINSEQ_1:22
.= len (MIM (FinS (F,D))) by RFINSEQ:def 2 ;
then A40: dom ((n |-> 0) ^ (MIM ((FinS (F,D)) /^ n))) = Seg (len (MIM (FinS (F,D)))) by FINSEQ_1:def 3;
A41: dom (n |-> 0) = Seg (len (n |-> 0)) by FINSEQ_1:def 3;

now :: thesis: for m being Nat st m in dom ((n |-> 0) ^ (MIM ((FinS (F,D)) /^ n))) holds
(((MIM (FinS (F,D))) (#) (CHI (A,C))) # c) . m = ((n |-> 0) ^ (MIM ((FinS (F,D)) /^ n))) . m

let m be Nat; :: thesis: ( m in dom ((n |-> 0) ^ (MIM ((FinS (F,D)) /^ n))) implies (((MIM (FinS (F,D))) (#) (CHI (A,C))) # c) . m = ((n |-> 0) ^ (MIM ((FinS (F,D)) /^ n))) . m )
reconsider m1 = m as Element of NAT by ORDINAL1:def 12;
reconsider r1 = (FinS (F,D)) . m as Real ;
assume A42: m in dom ((n |-> 0) ^ (MIM ((FinS (F,D)) /^ n))) ; :: thesis: (((MIM (FinS (F,D))) (#) (CHI (A,C))) # c) . m = ((n |-> 0) ^ (MIM ((FinS (F,D)) /^ n))) . m
then A43: 1 <= m by FINSEQ_3:25;
m in dom (MIM (FinS (F,D))) by A40, A42, FINSEQ_1:def 3;
then A44: m <= len (MIM (FinS (F,D))) by FINSEQ_3:25;
A45: (CHI (A,C)) . m = chi ((A . m),C) by A9, A7, A40, A42, RFUNCT_3:def 6;

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

per cases ( m <= n or n < m ) ;

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

reconsider r2 = (FinS (F,D)) . (m + 1) as Real ;
m < n + 1 by A46, NAT_1:13;
then m < len A by A33, XXREAL_0:2;
then m + 1 <= len A by NAT_1:13;
then m <= (len (MIM (FinS (F,D)))) - 1 by A7, A3, XREAL_1:19;
then (MIM (FinS (F,D))) . m1 = r1 - r2 by A43, RFINSEQ:def 2;
then ((MIM (FinS (F,D))) (#) (CHI (A,C))) . m = (r1 - r2) (#) (chi ((A . m),C)) by A2, A7, A6, A40, A42, A45, RFUNCT_3:def 7;
then A47: (((MIM (FinS (F,D))) (#) (CHI (A,C))) # c) . m = ((r1 - r2) (#) (chi ((A . m),C))) . c by A5, A7, A6, A8, A40, A42, RFUNCT_3:def 8;
not c in A . m by A1, A7, A3, A29, A40, A42, A46;
then A48: (chi ((A . m),C)) . c = 0 by RFUNCT_1:64;
A49: m in Seg n by A43, A46, FINSEQ_1:1;
A50: (n |-> 0) . m = 0 ;
dom ((r1 - r2) (#) (chi ((A . m),C))) = dom (chi ((A . m),C)) by VALUED_1:def 5
.= C by RFUNCT_1:61 ;
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 A38, A41, A48, A49, A50, FINSEQ_1:def 7 ;
:: thesis: verum

end;

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

then max (0,(m - n)) = m - n by FINSEQ_2:4;
then reconsider mn = m - n as Element of NAT by FINSEQ_2:5;
A52: n + 1 <= m by A51, NAT_1:13;
then c in A . m by A1, A7, A3, A35, A40, A42;
then A53: (chi ((A . m),C)) . c = 1 by RFUNCT_1:63;
A54: 1 <= mn by A52, XREAL_1:19;

now :: thesis: ( ( m = len (MIM (FinS (F,D))) & (((MIM (FinS (F,D))) (#) (CHI (A,C))) # c) . m = ((n |-> 0) ^ (MIM ((FinS (F,D)) /^ n))) . m ) or ( m <> len (MIM (FinS (F,D))) & (((MIM (FinS (F,D))) (#) (CHI (A,C))) # c) . m = ((n |-> 0) ^ (MIM ((FinS (F,D)) /^ n))) . m ) )

per cases ( m = len (MIM (FinS (F,D))) or m <> len (MIM (FinS (F,D))) ) ;

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

then (MIM (FinS (F,D))) . m = r1 by A4, RFINSEQ:def 2;
then ((MIM (FinS (F,D))) (#) (CHI (A,C))) . m = r1 (#) (chi ((A . m),C)) by A2, A7, A6, A40, A42, A45, RFUNCT_3:def 7;
then A56: (((MIM (FinS (F,D))) (#) (CHI (A,C))) # c) . m = (r1 (#) (chi ((A . m),C))) . c by A5, A7, A6, A8, A40, A42, RFUNCT_3:def 8;
A57: mn in dom ((MIM (FinS (F,D))) /^ n) by A28, A54, A55, FINSEQ_3:25;
A58: ((n |-> 0) ^ (MIM ((FinS (F,D)) /^ n))) . m = (MIM ((FinS (F,D)) /^ n)) . (m - n) by A38, A39, A44, A51, FINSEQ_1:24
.= ((MIM (FinS (F,D))) /^ n) . mn by RFINSEQ:15
.= (MIM (FinS (F,D))) . (mn + n) by A7, A3, A26, A57, RFINSEQ:def 1
.= r1 by A4, A55, RFINSEQ:def 2 ;
dom (r1 (#) (chi ((A . m),C))) = dom (chi ((A . m),C)) by VALUED_1:def 5
.= C by RFUNCT_1:61 ;
hence (((MIM (FinS (F,D))) (#) (CHI (A,C))) # c) . m = r1 * ((chi ((A . m),C)) . c) by A56, VALUED_1:def 5
.= ((n |-> 0) ^ (MIM ((FinS (F,D)) /^ n))) . m by A53, A58 ;
:: thesis: verum

end;

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

reconsider r2 = (FinS (F,D)) . (m + 1) as Real ;
m < len (MIM (FinS (F,D))) by A44, A59, XXREAL_0:1;
then m + 1 <= len (MIM (FinS (F,D))) by NAT_1:13;
then A60: m <= (len (MIM (FinS (F,D)))) - 1 by XREAL_1:19;
then (MIM (FinS (F,D))) . m1 = r1 - r2 by A43, RFINSEQ:def 2;
then ((MIM (FinS (F,D))) (#) (CHI (A,C))) . m = (r1 - r2) (#) (chi ((A . m),C)) by A2, A7, A6, A40, A42, A45, RFUNCT_3:def 7;
then A61: (((MIM (FinS (F,D))) (#) (CHI (A,C))) # c) . m = ((r1 - r2) (#) (chi ((A . m),C))) . c by A5, A7, A6, A8, A40, A42, RFUNCT_3:def 8;
mn <= len ((MIM (FinS (F,D))) /^ n) by A28, A44, XREAL_1:9;
then A62: mn in dom ((MIM (FinS (F,D))) /^ n) by A54, FINSEQ_3:25;
A63: ((n |-> 0) ^ (MIM ((FinS (F,D)) /^ n))) . m = (MIM ((FinS (F,D)) /^ n)) . (m - n) by A38, A39, A44, A51, FINSEQ_1:24
.= ((MIM (FinS (F,D))) /^ n) . mn by RFINSEQ:15
.= (MIM (FinS (F,D))) . (mn + n) by A7, A3, A26, A62, RFINSEQ:def 1
.= r1 - r2 by A43, A60, RFINSEQ:def 2 ;
dom ((r1 - r2) (#) (chi ((A . m),C))) = dom (chi ((A . m),C)) by VALUED_1:def 5
.= C by RFUNCT_1:61 ;
hence (((MIM (FinS (F,D))) (#) (CHI (A,C))) # c) . m = (r1 - r2) * ((chi ((A . m),C)) . c) by A61, VALUED_1:def 5
.= ((n |-> 0) ^ (MIM ((FinS (F,D)) /^ n))) . m by A53, A63 ;
:: thesis: verum

end;

end;

end;

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

end;

end;

end;

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

end;

hence ((MIM (FinS (F,D))) (#) (CHI (A,C))) # c = (n |-> 0) ^ (MIM ((FinS (F,D)) /^ n)) by A7, A6, A8, A39, FINSEQ_2:9; :: thesis: verum