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

A10: 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 );
A11: C = (Co_Gen B) . (len (Co_Gen B)) by Th3;
len (Co_Gen B) <> 0 by Th4;
then A12: 0 + 1 <= len (Co_Gen B) by NAT_1:13;
then A13: 1 in dom (Co_Gen B) by FINSEQ_3:27;
len (Co_Gen B) in dom (Co_Gen 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 (Co_Gen 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 (Co_Gen B) by A17, XXREAL_0:2;
m1 <= mi by A18, XREAL_1:21;
then A20: m1 <= len (Co_Gen B) by A17, XXREAL_0:2;

now

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

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

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

end;

case mi <> 1 ; :: thesis: (Rlor (F - r),B) . c = ((Rlor 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 (Co_Gen B) by A20, FINSEQ_3:27;
then not c in (Co_Gen B) . m1 by A15, XREAL_1:46;
then c in ((Co_Gen B) . (m1 + 1)) \ ((Co_Gen B) . m1) by A15, XBOOLE_0:def 5;
then A25: ( (Rlor (F - r),B) . c = (FinS (F - r),D) . (m1 + 1) & (Rlor F,B) . c = (FinS F,D) . (m1 + 1) ) by A1, A2, A7, A19, A24, Th22;
m1 + 1 in Seg (card D) by A2, A4, 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, A8, A4, A15, FINSEQ_3:31;
hence (Rlor (F - r),B) . c = ((Rlor F,B) . c) - r by A9, A25, A26, VALUED_1:13
.= ((Rlor F,B) - r) . c by A3, VALUED_1:3 ;
:: thesis: verum

end;

end;

end;

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

end;

dom ((Rlor F,B) - r) = C by A3, VALUED_1:3;
hence Rlor (F - r),B = (Rlor F,B) - r by A2, A7, A10, Th21, PARTFUN1:34; :: thesis: verum