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
Rlor (F - r),A = (Rlor 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
Rlor (F - r),A = (Rlor 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
Rlor (F - r),A = (Rlor F,A) - r
let B be RearrangmentGen of C; :: thesis: ( F is total & card D = card C implies Rlor (F - r),B = (Rlor F,B) - r )
assume A1: ( F is total & card D = card C ) ; :: thesis: Rlor (F - r),B = (Rlor F,B) - r
set b = Co_Gen B;
A2: dom F = D by A1, PARTFUN1:def 4;
then A3: dom (F - r) = D by VALUED_1:3;
then A4: F - r is total by PARTFUN1:def 4;
then A5: ( dom (Rlor (F - r),B) = C & dom (Rlor F,B) = C ) by A1, Th21;
then A6: dom ((Rlor F,B) - r) = C by VALUED_1:3;
A7: ( F | D = F & (F - r) | D = F - r ) by A2, A3, RELAT_1:97;
then A8: FinS (F - r),D = (FinS F,D) - ((card D) |-> r) by A2, RFUNCT_3:76;
A9: ( len (FinS (F - r),D) = card D & len (FinS F,D) = card D & len ((card D) |-> r) = card D ) by A2, A3, A7, FINSEQ_1:def 18, RFUNCT_3:70;
A10: ( len B = card C & len (Co_Gen B) = card C ) by Th1;

now

let c be Element of C; :: thesis: ( c in dom (Rlor (F - r),B) implies (Rlor (F - r),B) . c = ((Rlor F,B) - r) . c )
assume c in dom (Rlor (F - r),B) ; :: thesis: (Rlor (F - r),B) . c = ((Rlor F,B) - r) . c
defpred S₁[ set ] means ( $1 in dom (Co_Gen B) & c in (Co_Gen B) . $1 );
len (Co_Gen B) <> 0 by Th4;
then 0 < len (Co_Gen B) ;
then A11: 0 + 1 <= len (Co_Gen B) by NAT_1:13;
then A12: ( len (Co_Gen B) in dom (Co_Gen B) & 1 in dom (Co_Gen B) ) by FINSEQ_3:27;
C = (Co_Gen B) . (len (Co_Gen B)) by Th3;
then A13: ex n being Nat st S₁[n] by A12;
consider mi being Nat such that
A14: ( S₁[mi] & ( for n being Nat st S₁[n] holds
mi <= n ) ) from NAT_1:sch 5(A13);
A15: ( 1 <= mi & mi <= len (Co_Gen B) ) by A14, 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;
( m1 <= (len (Co_Gen B)) - 1 & mi < mi + 1 & mi <= mi + 1 ) by A15, NAT_1:13, XREAL_1:11;
then ( m1 <= mi & m1 < mi ) by XREAL_1:21;
then A16: ( m1 <= len (Co_Gen B) & m1 < len (Co_Gen B) ) by A15, XXREAL_0:2;

now

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

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

then A17: ( (Rlor (F - r),B) . c = (FinS (F - r),D) . 1 & (Rlor F,B) . c = (FinS F,D) . 1 ) by A1, A4, A14, Th22;
A18: 1 in dom (FinS (F - r),D) by A1, A9, A10, A11, FINSEQ_3:27;
1 in Seg (card D) by A1, A10, A12, FINSEQ_1:def 3;
then ((card D) |-> r) . 1 = r by FUNCOP_1:13;
hence (Rlor (F - r),B) . c = ((Rlor F,B) . c) - r by A8, A17, A18, VALUED_1:13
.= ((Rlor F,B) - r) . c by A5, VALUED_1:3 ;
:: thesis: verum

end;

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

then 1 < mi by A15, XXREAL_0:1;
then 1 + 1 <= mi by NAT_1:13;
then A19: 1 <= m1 by XREAL_1:21;
then m1 in dom (Co_Gen B) by A16, FINSEQ_3:27;
then not c in (Co_Gen B) . m1 by A14, XREAL_1:46;
then c in ((Co_Gen B) . (m1 + 1)) \ ((Co_Gen B) . m1) by A14, XBOOLE_0:def 5;
then A20: ( (Rlor (F - r),B) . c = (FinS (F - r),D) . (m1 + 1) & (Rlor F,B) . c = (FinS F,D) . (m1 + 1) ) by A1, A4, A16, A19, Th22;
A21: m1 + 1 in dom (FinS (F - r),D) by A1, A9, A10, A14, FINSEQ_3:31;
m1 + 1 in Seg (card D) by A1, A10, A14, FINSEQ_1:def 3;
then ((card D) |-> r) . (m1 + 1) = r by FUNCOP_1:13;
hence (Rlor (F - r),B) . c = ((Rlor F,B) . c) - r by A8, A20, A21, VALUED_1:13
.= ((Rlor F,B) - r) . c by A5, VALUED_1:3 ;
:: thesis: verum

end;

end;

end;

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

end;

hence Rlor (F - r),B = (Rlor F,B) - r by A5, A6, PARTFUN1:34; :: thesis: verum