let r be Real; :: thesis: for D, C being non empty finite set
for F being PartFunc of D,REAL
for A being RearrangmentGen of C st F is total & card D = card C holds
Rland (F - r),A = (Rland F,A) - r
let D, C be non empty finite set ; :: thesis: for F being PartFunc of D,REAL
for A being RearrangmentGen of C st F is total & card D = card C holds
Rland (F - r),A = (Rland F,A) - r
let F be PartFunc of D,REAL ; :: thesis: for A being RearrangmentGen of C st F is total & card D = card C holds
Rland (F - r),A = (Rland F,A) - r
let B be RearrangmentGen of C; :: thesis: ( F is total & card D = card C implies Rland (F - r),B = (Rland F,B) - r )
assume that
A1: F is total and
A2: card D = card C ; :: thesis: Rland (F - r),B = (Rland F,B) - r
A3: dom (Rland F,B) = C by A1, A2, Th13;
A4: dom F = D by A1, PARTFUN1:def 4;
then A5: dom (F - r) = D by VALUED_1:3;
then A6: F - r is total by PARTFUN1:def 4;
(F - r) | D = F - r by A5, RELAT_1:97;
then A7: len (FinS (F - r),D) = card D by A5, RFUNCT_3:70;
A8: len B = card C by Th1;
F | D = F by A4, RELAT_1:97;
then A9: FinS (F - r),D = (FinS F,D) - ((card D) |-> r) by A4, RFUNCT_3:76;

A10: now

let c be Element of C; :: thesis: ( c in dom (Rland (F - r),B) implies (Rland (F - r),B) . c = ((Rland F,B) - r) . c )
assume c in dom (Rland (F - r),B) ; :: thesis: (Rland (F - r),B) . c = ((Rland F,B) - r) . c
defpred S₁[ set ] means ( $1 in dom B & c in B . $1 );
A11: C = B . (len B) by Th3;
len B <> 0 by Th4;
then A12: 0 + 1 <= len B by NAT_1:13;
then A13: 1 in dom B by FINSEQ_3:27;
len B in dom B by A12, FINSEQ_3:27;
then A14: ex n being Nat st S₁[n] by A11;
consider mi being Nat such that
A15: ( S₁[mi] & ( for n being Nat st S₁[n] holds
mi <= n ) ) from NAT_1:sch 5(A14);
A16: 1 <= mi by A15, FINSEQ_3:27;
then max 0 ,(mi - 1) = mi - 1 by FINSEQ_2:4;
then reconsider m1 = mi - 1 as Element of NAT by FINSEQ_2:5;
A17: mi <= len B by A15, FINSEQ_3:27;
A18: mi < mi + 1 by NAT_1:13;
then m1 < mi by XREAL_1:21;
then A19: m1 < len B by A17, XXREAL_0:2;
m1 <= mi by A18, XREAL_1:21;
then A20: m1 <= len B by A17, XXREAL_0:2;

now

per cases ( mi = 1 or mi <> 1 ) ;

case A21: mi = 1 ; :: thesis: (Rland (F - r),B) . c = ((Rland F,B) - r) . c

A22: 1 in dom (FinS (F - r),D) by A2, A7, A8, A12, FINSEQ_3:27;
1 in Seg (card D) by A2, A8, A13, FINSEQ_1:def 3;
then A23: ((card D) |-> r) . 1 = r by FUNCOP_1:13;
( (Rland (F - r),B) . c = (FinS (F - r),D) . 1 & (Rland F,B) . c = (FinS F,D) . 1 ) by A1, A2, A6, A15, A21, Th15;
hence (Rland (F - r),B) . c = ((Rland F,B) . c) - r by A9, A22, A23, VALUED_1:13
.= ((Rland F,B) - r) . c by A3, VALUED_1:3 ;
:: thesis: verum

end;

case mi <> 1 ; :: thesis: (Rland (F - r),B) . c = ((Rland F,B) - r) . c

then 1 < mi by A16, XXREAL_0:1;
then 1 + 1 <= mi by NAT_1:13;
then A24: 1 <= m1 by XREAL_1:21;
then m1 in dom B by A20, FINSEQ_3:27;
then not c in B . m1 by A15, XREAL_1:46;
then c in (B . (m1 + 1)) \ (B . m1) by A15, XBOOLE_0:def 5;
then A25: ( (Rland (F - r),B) . c = (FinS (F - r),D) . (m1 + 1) & (Rland F,B) . c = (FinS F,D) . (m1 + 1) ) by A1, A2, A6, A19, A24, Th15;
m1 + 1 in Seg (card D) by A2, A8, A15, FINSEQ_1:def 3;
then A26: ((card D) |-> r) . (m1 + 1) = r by FUNCOP_1:13;
m1 + 1 in dom (FinS (F - r),D) by A2, A7, A8, A15, FINSEQ_3:31;
hence (Rland (F - r),B) . c = ((Rland F,B) . c) - r by A9, A25, A26, VALUED_1:13
.= ((Rland F,B) - r) . c by A3, VALUED_1:3 ;
:: thesis: verum

end;

end;

end;

hence (Rland (F - r),B) . c = ((Rland F,B) - r) . c ; :: thesis: verum

end;

dom ((Rland F,B) - r) = C by A3, VALUED_1:3;
hence Rland (F - r),B = (Rland F,B) - r by A2, A6, A10, Th13, PARTFUN1:34; :: thesis: verum