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