let r be Real; 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
Rlor ((F - r),A) = (Rlor (F,A)) - r
let C, D be 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 F be 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 B be RearrangmentGen of C; ( 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
; Rlor ((F - r),B) = (Rlor (F,B)) - r
A3:
dom (Rlor (F,B)) = C
by A1, A2, Th20;
set b = Co_Gen B;
A4:
len (Co_Gen B) = card C
by Th1;
A5:
dom F = D
by A1, PARTFUN1:def 2;
then A6:
dom (F - r) = D
by VALUED_1:3;
then A7:
F - r is total
by PARTFUN1:def 2;
(F - r) | D = F - r
by A6, RELAT_1:68;
then A8:
len (FinS ((F - r),D)) = card D
by A6, RFUNCT_3:67;
reconsider rr = r as Element of REAL by XREAL_0:def 1;
F | D = F
by A5, RELAT_1:68;
then A9:
FinS ((F - r),D) = (FinS (F,D)) - ((card D) |-> rr)
by A5, RFUNCT_3:73;
A10:
now for c being Element of C st c in dom (Rlor ((F - r),B)) holds
(Rlor ((F - r),B)) . c = ((Rlor (F,B)) - r) . clet c be
Element of
C;
( 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))
;
(Rlor ((F - r),B)) . c = ((Rlor (F,B)) - r) . cdefpred S1[
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:25;
len (Co_Gen B) in dom (Co_Gen B)
by A12, FINSEQ_3:25;
then A14:
ex
n being
Nat st
S1[
n]
by A11;
consider mi being
Nat such that A15:
(
S1[
mi] & ( for
n being
Nat st
S1[
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 (Co_Gen 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 (Co_Gen B)
by A17, XXREAL_0:2;
m1 <= mi
by A18, XREAL_1:19;
then A20:
m1 <= len (Co_Gen B)
by A17, XXREAL_0:2;
now ( ( mi = 1 & (Rlor ((F - r),B)) . c = ((Rlor (F,B)) - r) . c ) or ( mi <> 1 & (Rlor ((F - r),B)) . c = ((Rlor (F,B)) - r) . c ) )per cases
( mi = 1 or mi <> 1 )
;
case A21:
mi = 1
;
(Rlor ((F - r),B)) . c = ((Rlor (F,B)) - r) . cA22:
1
in dom (FinS ((F - r),D))
by A2, A8, A4, A12, FINSEQ_3:25;
1
in Seg (card D)
by A2, A4, A13, FINSEQ_1:def 3;
then A23:
((card D) |-> r) . 1
= r
by FUNCOP_1:7;
(
(Rlor ((F - r),B)) . c = (FinS ((F - r),D)) . 1 &
(Rlor (F,B)) . c = (FinS (F,D)) . 1 )
by A1, A2, A7, A15, A21, Th21;
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
;
verum end; case
mi <> 1
;
(Rlor ((F - r),B)) . c = ((Rlor (F,B)) - r) . cthen
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 (Co_Gen B)
by A20, FINSEQ_3:25;
then
not
c in (Co_Gen B) . m1
by A15, XREAL_1:44;
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, Th21;
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:7;
m1 + 1
in dom (FinS ((F - r),D))
by A2, A8, A4, A15, FINSEQ_3:29;
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
;
verum end; hence
(Rlor ((F - r),B)) . c = ((Rlor (F,B)) - r) . c
;
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, Th20, PARTFUN1:5; verum