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 C = card D holds
rng (Rlor (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 (Rlor (F,A)) = rng (FinS (F,D))
let B be RearrangmentGen of C; ( F is total & card C = card D implies rng (Rlor (F,B)) = rng (FinS (F,D)) )
assume that
A1:
F is total
and
A2:
card C = card D
; rng (Rlor (F,B)) = rng (FinS (F,D))
set fd = FinS (F,D);
set p = Rlor (F,B);
set mf = MIM (FinS (F,D));
set b = Co_Gen B;
set h = CHI ((Co_Gen B),C);
A3:
len (MIM (FinS (F,D))) = len (CHI ((Co_Gen B),C))
by A1, A2, Th11;
dom F is finite
;
then reconsider F9 = F as finite Function by FINSET_1:10;
A4:
dom (FinS (F,D)) = Seg (len (FinS (F,D)))
by FINSEQ_1:def 3;
A5:
dom (Rlor (F,B)) = C
by A1, A2, Th20;
A6:
dom (Co_Gen B) = Seg (len (Co_Gen B))
by FINSEQ_1:def 3;
reconsider dfd = dom (FinS (F,D)), dF = dom F9 as finite set ;
A7:
( len (CHI ((Co_Gen B),C)) = len (Co_Gen B) & len (MIM (FinS (F,D))) = len (FinS (F,D)) )
by RFINSEQ:def 2, RFUNCT_3:def 6;
A8:
dom F = D
by A1, PARTFUN1:def 2;
then
F | D = F
by RELAT_1:68;
then
FinS (F,D),F are_fiberwise_equipotent
by A8, RFUNCT_3:def 13;
then
card dfd = card dF
by CLASSES1:81;
then
len (FinS (F,D)) <> 0
by A8, A4;
then A9:
0 + 1 <= len (FinS (F,D))
by NAT_1:13;
then A10:
1 in dom (FinS (F,D))
by FINSEQ_3:25;
thus
rng (Rlor (F,B)) c= rng (FinS (F,D))
XBOOLE_0:def 10 rng (FinS (F,D)) c= rng (Rlor (F,B))proof
let x be
object ;
TARSKI:def 3 ( not x in rng (Rlor (F,B)) or x in rng (FinS (F,D)) )
assume
x in rng (Rlor (F,B))
;
x in rng (FinS (F,D))
then consider c being
Element of
C such that
c in dom (Rlor (F,B))
and A11:
(Rlor (F,B)) . c = x
by PARTFUN1:3;
defpred S1[
set ]
means ( $1
in dom (Co_Gen B) &
c in (Co_Gen 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: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;
A15:
mi <= len (Co_Gen B)
by A13, FINSEQ_3:25;
now ( ( mi = 1 & x in rng (FinS (F,D)) ) or ( mi <> 1 & x in rng (FinS (F,D)) ) )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:19;
A17:
m1 < mi
by XREAL_1:44;
then
m1 <= len (Co_Gen B)
by A15, XXREAL_0:2;
then
m1 in dom (Co_Gen B)
by A16, FINSEQ_3:25;
then
not
c in (Co_Gen B) . m1
by A13, XREAL_1:44;
then A18:
c in ((Co_Gen B) . (m1 + 1)) \ ((Co_Gen B) . m1)
by A13, XBOOLE_0:def 5;
m1 < len (Co_Gen B)
by A15, A17, XXREAL_0:2;
then
(Rlor (F,B)) . c = (FinS (F,D)) . (m1 + 1)
by A1, A2, A16, A18, Th21;
hence
x in rng (FinS (F,D))
by A3, A7, A4, A6, A11, A13, FUNCT_1:def 3;
verum end;
hence
x in rng (FinS (F,D))
;
verum
end;
let x be object ; TARSKI:def 3 ( not x in rng (FinS (F,D)) or x in rng (Rlor (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 (Rlor (F,B))
then A19:
ex n being Nat st S1[n]
by FINSEQ_2:10;
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: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;
A22:
mi <= len (FinS (F,D))
by A20, FINSEQ_3:25;
now ( ( mi = 1 & x in rng (Rlor (F,B)) ) or ( mi <> 1 & x in rng (Rlor (F,B)) ) )per cases
( mi = 1 or mi <> 1 )
;
case A23:
mi = 1
;
x in rng (Rlor (F,B))set y = the
Element of
(Co_Gen B) . 1;
A24:
(Co_Gen B) . 1
<> {}
by A3, A7, A4, A6, A10, Th7;
(Co_Gen B) . 1
c= C
by A3, A7, A4, A6, A10, Lm5;
then reconsider y = the
Element of
(Co_Gen B) . 1 as
Element of
C by A24;
(Rlor (F,B)) . y = (FinS (F,D)) . 1
by A1, A2, A24, Th21;
hence
x in rng (Rlor (F,B))
by A5, A20, A23, FUNCT_1:def 3;
verum end; case A25:
mi <> 1
;
x in rng (Rlor (F,B))set y = the
Element of
((Co_Gen B) . (m1 + 1)) \ ((Co_Gen 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:19;
m1 + 1
<= len (FinS (F,D))
by A20, FINSEQ_3:25;
then
m1 <= (len (FinS (F,D))) - 1
by XREAL_1:19;
then A27:
((Co_Gen B) . (m1 + 1)) \ ((Co_Gen B) . m1) <> {}
by A3, A7, A26, Th8;
then A28:
the
Element of
((Co_Gen B) . (m1 + 1)) \ ((Co_Gen B) . m1) in (Co_Gen B) . (m1 + 1)
by XBOOLE_0:def 5;
(Co_Gen B) . mi c= C
by A3, A7, A4, A6, A20, Lm5;
then reconsider y = the
Element of
((Co_Gen B) . (m1 + 1)) \ ((Co_Gen B) . m1) as
Element of
C by A28;
m1 < mi
by XREAL_1:44;
then
m1 < len (FinS (F,D))
by A22, XXREAL_0:2;
then
(Rlor (F,B)) . y = (FinS (F,D)) . (m1 + 1)
by A1, A2, A3, A7, A26, A27, Th21;
hence
x in rng (Rlor (F,B))
by A5, A20, FUNCT_1:def 3;
verum end;
hence
x in rng (Rlor (F,B))
; verum