let r be Real; :: thesis: for C, D 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 C, D 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, Th12;
A4: dom F = D by A1, PARTFUN1:def 2;
then A5: dom (F - r) = D by VALUED_1:3;
then A6: F - r is total by PARTFUN1:def 2;
(F - r) | D = F - r by A5, RELAT_1:68;
then A7: len (FinS ((F - r),D)) = card D by A5, RFUNCT_3:67;
A8: len B = card C by Th1;
reconsider rr = r as Element of REAL by XREAL_0:def 1;
F | D = F by A4, RELAT_1:68;
then A9: FinS ((F - r),D) = (FinS (F,D)) - ((card D) |-> rr) by A4, RFUNCT_3:73;

A10: now :: thesis: for c being Element of C st c in dom (Rland ((F - r),B)) holds
(Rland ((F - r),B)) . c = ((Rland (F,B)) - r) . c

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:25;
len B in dom B by A12, FINSEQ_3:25;
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:25;
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:25;
A18: mi < mi + 1 by NAT_1:13;
then m1 < mi by XREAL_1:19;
then A19: m1 < len B by A17, XXREAL_0:2;
m1 <= mi by A18, XREAL_1:19;
then A20: m1 <= len B by A17, XXREAL_0:2;

now :: thesis: ( ( mi = 1 & (Rland ((F - r),B)) . c = ((Rland (F,B)) - r) . c ) or ( mi <> 1 & (Rland ((F - r),B)) . c = ((Rland (F,B)) - r) . c ) )

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:25;
1 in Seg (card D) by A2, A8, A13, FINSEQ_1:def 3;
then A23: ((card D) |-> r) . 1 = r by FUNCOP_1:7;
( (Rland ((F - r),B)) . c = (FinS ((F - r),D)) . 1 & (Rland (F,B)) . c = (FinS (F,D)) . 1 ) by A1, A2, A6, A15, A21, Th14;
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:19;
then m1 in dom B by A20, FINSEQ_3:25;
then not c in B . m1 by A15, XREAL_1:44;
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, Th14;
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:7;
m1 + 1 in dom (FinS ((F - r),D)) by A2, A7, A8, A15, FINSEQ_3:29;
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, Th12, PARTFUN1:5; :: thesis: verum