let D, C be non empty finite set ; for F being PartFunc of D,REAL
for A being RearrangmentGen of C st F is total & card C = card D holds
rng (Rland F,A) = rng (FinS F,D)
let F be PartFunc of D,REAL ; for A being RearrangmentGen of C st F is total & card C = card D holds
rng (Rland F,A) = rng (FinS F,D)
let B be RearrangmentGen of C; ( F is total & card C = card D implies rng (Rland F,B) = rng (FinS F,D) )
assume that
A1:
F is total
and
A2:
card C = card D
; rng (Rland F,B) = rng (FinS F,D)
set fd = FinS F,D;
set p = Rland F,B;
set mf = MIM (FinS F,D);
set h = CHI B,C;
A3:
len (MIM (FinS F,D)) = len (CHI B,C)
by A1, A2, Th12;
A4:
dom F = D
by A1, PARTFUN1:def 4;
then reconsider fd9 = FinS F,D, F9 = F as finite Function by FINSET_1:29;
reconsider dfd = dom fd9, dF = dom F9 as finite set ;
A5:
( len (CHI B,C) = len B & len (MIM (FinS F,D)) = len (FinS F,D) )
by RFINSEQ:def 3, RFUNCT_3:def 6;
A6:
dom (Rland F,B) = C
by A1, A2, Th13;
A7:
dom (FinS F,D) = Seg (len (FinS F,D))
by FINSEQ_1:def 3;
A8:
dom B = Seg (len B)
by FINSEQ_1:def 3;
F | D = F
by A4, RELAT_1:97;
then
FinS F,D,F are_fiberwise_equipotent
by A4, RFUNCT_3:def 14;
then
card dfd = card dF
by CLASSES1:89;
then
len (FinS F,D) <> 0
by A4, A7;
then A9:
0 + 1 <= len (FinS F,D)
by NAT_1:13;
then A10:
1 in dom (FinS F,D)
by FINSEQ_3:27;
thus
rng (Rland F,B) c= rng (FinS F,D)
XBOOLE_0:def 10 rng (FinS F,D) c= rng (Rland F,B)proof
let x be
set ;
TARSKI:def 3 ( not x in rng (Rland F,B) or x in rng (FinS F,D) )
assume
x in rng (Rland F,B)
;
x in rng (FinS F,D)
then consider c being
Element of
C such that
c in dom (Rland F,B)
and A11:
(Rland F,B) . c = x
by PARTFUN1:26;
defpred S1[
set ]
means ( $1
in dom B &
c in B . $1 );
A12:
ex
n being
Nat st
S1[
n]
consider mi being
Nat such that A13:
(
S1[
mi] & ( for
n being
Nat st
S1[
n] holds
mi <= n ) )
from NAT_1:sch 5(A12);
A14:
1
<= mi
by A13, 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;
A15:
mi <= len B
by A13, FINSEQ_3:27;
now per cases
( mi = 1 or mi <> 1 )
;
case
mi <> 1
;
x in rng (FinS F,D)then
1
< mi
by A14, XXREAL_0:1;
then
1
+ 1
<= mi
by NAT_1:13;
then A16:
1
<= m1
by XREAL_1:21;
A17:
m1 < mi
by XREAL_1:46;
then
m1 <= len B
by A15, XXREAL_0:2;
then
m1 in dom B
by A16, FINSEQ_3:27;
then
not
c in B . m1
by A13, XREAL_1:46;
then A18:
c in (B . (m1 + 1)) \ (B . m1)
by A13, XBOOLE_0:def 5;
m1 < len B
by A15, A17, XXREAL_0:2;
then
(Rland F,B) . c = (FinS F,D) . (m1 + 1)
by A1, A2, A16, A18, Th15;
hence
x in rng (FinS F,D)
by A3, A5, A7, A8, A11, A13, FUNCT_1:def 5;
verum end;
hence
x in rng (FinS F,D)
;
verum
end;
let x be set ; TARSKI:def 3 ( not x in rng (FinS F,D) or x in rng (Rland F,B) )
defpred S1[ Nat] means ( $1 in dom (FinS F,D) & (FinS F,D) . $1 = x );
assume
x in rng (FinS F,D)
; x in rng (Rland F,B)
then A19:
ex n being Nat st S1[n]
by FINSEQ_2:11;
consider mi being Nat such that
A20:
( S1[mi] & ( for n being Nat st S1[n] holds
mi <= n ) )
from NAT_1:sch 5(A19);
A21:
1 <= mi
by A20, 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;
A22:
mi <= len (FinS F,D)
by A20, FINSEQ_3:27;
now per cases
( mi = 1 or mi <> 1 )
;
case A23:
mi = 1
;
x in rng (Rland F,B)consider y being
Element of
B . 1;
A24:
B . 1
<> {}
by A3, A5, A7, A8, A10, Th7;
B . 1
c= C
by A3, A5, A7, A8, A10, Lm5;
then reconsider y =
y as
Element of
C by A24, TARSKI:def 3;
(Rland F,B) . y = (FinS F,D) . 1
by A1, A2, A24, Th15;
hence
x in rng (Rland F,B)
by A6, A20, A23, FUNCT_1:def 5;
verum end; case A25:
mi <> 1
;
x in rng (Rland F,B)consider y being
Element of
(B . (m1 + 1)) \ (B . m1);
1
< mi
by A21, A25, XXREAL_0:1;
then
1
+ 1
<= mi
by NAT_1:13;
then A26:
1
<= m1
by XREAL_1:21;
m1 + 1
<= len (FinS F,D)
by A20, FINSEQ_3:27;
then
m1 <= (len (FinS F,D)) - 1
by XREAL_1:21;
then A27:
(B . (m1 + 1)) \ (B . m1) <> {}
by A3, A5, A26, Th8;
then A28:
y in B . (m1 + 1)
by XBOOLE_0:def 5;
B . mi c= C
by A3, A5, A7, A8, A20, Lm5;
then reconsider y =
y as
Element of
C by A28;
m1 < mi
by XREAL_1:46;
then
m1 < len (FinS F,D)
by A22, XXREAL_0:2;
then
(Rland F,B) . y = (FinS F,D) . (m1 + 1)
by A1, A2, A3, A5, A26, A27, Th15;
hence
x in rng (Rland F,B)
by A6, A20, FUNCT_1:def 5;
verum end;
hence
x in rng (Rland F,B)
; verum