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 (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 that
A1: F is total and
A2: 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);
A3: len (MIM (FinS (F,D))) = len (CHI (B,C)) by A1, A2, Th11;
A4: dom F = D by A1, PARTFUN1:def 2;
then reconsider fd9 = FinS (F,D), F9 = F as finite Function by FINSET_1:10;
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 2, RFUNCT_3:def 6;
A6: dom (Rland (F,B)) = C by A1, A2, Th12;
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:68;
then FinS (F,D),F are_fiberwise_equipotent by A4, RFUNCT_3:def 13;
then card dfd = card dF by CLASSES1:81;
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:25;
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 object ; :: 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
c in dom (Rland (F,B)) and
A11: (Rland (F,B)) . c = x by PARTFUN1:3;
defpred S₁[ set ] means ( $1 in dom B & c in B . $1 );
A12: ex n being Nat st S₁[n]

proof

take n = len B; :: thesis: S₁[n]
B . n = C by Th3;
hence S₁[n] by A3, A5, 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 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 (Rland (F,B)) . c = (FinS (F,D)) . 1 by A1, A2, A13, Th14;
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 B by A15, XXREAL_0:2;
then m1 in dom B by A16, FINSEQ_3:25;
then not c in B . m1 by A13, XREAL_1:44;
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, Th14;
hence x in rng (FinS (F,D)) by A3, A5, A7, A8, 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 (Rland (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 (Rland (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 (Rland (F,B)) ) or ( mi <> 1 & x in rng (Rland (F,B)) ) )

per cases ( mi = 1 or mi <> 1 ) ;

case A23: mi = 1 ; :: thesis: x in rng (Rland (F,B))

set y = the 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 = the Element of B . 1 as Element of C by A24;
(Rland (F,B)) . y = (FinS (F,D)) . 1 by A1, A2, A24, Th14;
hence x in rng (Rland (F,B)) by A6, A20, A23, FUNCT_1:def 3; :: thesis: verum

end;

case A25: mi <> 1 ; :: thesis: x in rng (Rland (F,B))

set y = the 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: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: (B . (m1 + 1)) \ (B . m1) <> {} by A3, A5, A26, Th8;
then A28: the Element of (B . (m1 + 1)) \ (B . m1) in B . (m1 + 1) by XBOOLE_0:def 5;
B . mi c= C by A3, A5, A7, A8, A20, Lm5;
then reconsider y = the Element of (B . (m1 + 1)) \ (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 (Rland (F,B)) . y = (FinS (F,D)) . (m1 + 1) by A1, A2, A3, A5, A26, A27, Th14;
hence x in rng (Rland (F,B)) by A6, A20, FUNCT_1:def 3; :: thesis: verum

end;

end;

end;

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