let C, D 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 (Rlor (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 (Rlor (F,A)) = rng (FinS (F,D))
let B be RearrangmentGen of C; :: thesis: ( 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 ; :: thesis: 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)) :: according to XBOOLE_0:def 10 :: thesis: rng (FinS (F,D)) c= rng (Rlor (F,B))

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (Rlor (F,B)) or x in rng (FinS (F,D)) )
assume x in rng (Rlor (F,B)) ; :: thesis: 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 S₁[ set ] means ( $1 in dom (Co_Gen B) & c in (Co_Gen B) . $1 );
A12: ex n being Nat st S₁[n]

proof

take n = len (Co_Gen B); :: thesis: S₁[n]
(Co_Gen B) . n = C by Th3;
hence S₁[n] by A3, A7, A9, FINSEQ_3:25; :: thesis: verum

end;

consider mi being Nat such that
A13: ( S₁[mi] & ( for n being Nat st S₁[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 :: thesis: ( ( 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 ; :: thesis: x in rng (FinS (F,D))

then (Rlor (F,B)) . c = (FinS (F,D)) . 1 by A1, A2, A13, Th21;
hence x in rng (FinS (F,D)) by A10, A11, FUNCT_1:def 3; :: thesis: verum

end;

case mi <> 1 ; :: thesis: 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; :: thesis: verum

end;

end;

end;

hence x in rng (FinS (F,D)) ; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (FinS (F,D)) or x in rng (Rlor (F,B)) )
defpred S₁[ Nat] means ( $1 in dom (FinS (F,D)) & (FinS (F,D)) . $1 = x );
assume x in rng (FinS (F,D)) ; :: thesis: x in rng (Rlor (F,B))
then A19: ex n being Nat st S₁[n] by FINSEQ_2:10;
consider mi being Nat such that
A20: ( S₁[mi] & ( for n being Nat st S₁[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 :: thesis: ( ( 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 ; :: thesis: 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; :: thesis: verum

end;

case A25: mi <> 1 ; :: thesis: 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; :: thesis: verum

end;

end;

end;

hence x in rng (Rlor (F,B)) ; :: thesis: verum