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
Rland ((F - r),A) = (Rland (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
Rland ((F - r),A) = (Rland (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
Rland ((F - r),A) = (Rland (F,A)) - r
let B be RearrangmentGen of C; ( 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
; 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 for c being Element of C st c in dom (Rland ((F - r),B)) holds
(Rland ((F - r),B)) . c = ((Rland (F,B)) - r) . clet c be
Element of
C;
( 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))
;
(Rland ((F - r),B)) . c = ((Rland (F,B)) - r) . cdefpred S1[
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
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 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 ( ( 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
;
(Rland ((F - r),B)) . c = ((Rland (F,B)) - r) . cA22:
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
;
verum end; case
mi <> 1
;
(Rland ((F - r),B)) . c = ((Rland (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 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
;
verum end; hence
(Rland ((F - r),B)) . c = ((Rland (F,B)) - r) . c
;
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; verum