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
Rland (F,A), FinS (F,D) are_fiberwise_equipotent
let F be PartFunc of D,REAL; :: thesis: for A being RearrangmentGen of C st F is total & card C = card D holds
Rland (F,A), FinS (F,D) are_fiberwise_equipotent
let B be RearrangmentGen of C; :: thesis: ( F is total & card C = card D implies Rland (F,B), FinS (F,D) are_fiberwise_equipotent )
set fd = FinS (F,D);
set p = Rland (F,B);
set mf = MIM (FinS (F,D));
set h = CHI (B,C);
dom (Rland (F,B)) is finite ;
then reconsider p = Rland (F,B) as finite PartFunc of C,REAL by FINSET_1:10;
A1: ( len (CHI (B,C)) = len B & len (MIM (FinS (F,D))) = len (FinS (F,D)) ) by RFINSEQ:def 2, RFUNCT_3:def 6;
A2: ( dom (FinS (F,D)) = Seg (len (FinS (F,D))) & dom B = Seg (len B) ) by FINSEQ_1:def 3;
assume A3: ( F is total & card C = card D ) ; :: thesis: Rland (F,B), FinS (F,D) are_fiberwise_equipotent
then A4: len (MIM (FinS (F,D))) = len (CHI (B,C)) by Th11;
A5: dom p = C by A3, Th12;
A6: rng p = rng (FinS (F,D)) by A3, Th15;

now :: thesis: for x being object holds card (Coim ((FinS (F,D)),x)) = card (Coim (p,x))

let x be object ; :: thesis: card (Coim ((FinS (F,D)),x)) = card (Coim (p,x))

now :: thesis: ( ( not x in rng (FinS (F,D)) & card ((FinS (F,D)) " {x}) = card (p " {x}) ) or ( x in rng (FinS (F,D)) & card ((FinS (F,D)) " {x}) = card (p " {x}) ) )

per cases ( not x in rng (FinS (F,D)) or x in rng (FinS (F,D)) ) ;

case A7: not x in rng (FinS (F,D)) ; :: thesis: card ((FinS (F,D)) " {x}) = card (p " {x})

then (FinS (F,D)) " {x} = {} by Lm1;
hence card ((FinS (F,D)) " {x}) = card (p " {x}) by A6, A7, Lm1; :: thesis: verum

end;

case A8: x in rng (FinS (F,D)) ; :: thesis: card ((FinS (F,D)) " {x}) = card (p " {x})

defpred S₁[ Nat] means ( $1 in dom (FinS (F,D)) & (FinS (F,D)) . $1 = x );
A9: for n being Nat st S₁[n] holds
n <= len (FinS (F,D)) by FINSEQ_3:25;
A10: ex n being Nat st S₁[n] by A8, FINSEQ_2:10;
consider ma being Nat such that
A11: ( S₁[ma] & ( for n being Nat st S₁[n] holds
n <= ma ) ) from NAT_1:sch 6(A9, A10);
A12: ex n being Nat st S₁[n] by A8, FINSEQ_2:10;
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);
reconsider r = x as Real by A13;
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: m1 + 1 = mi ;
A16: ma <= len (FinS (F,D)) by A11, FINSEQ_3:25;
A17: (Seg ma) \ (Seg m1) = (FinS (F,D)) " {x}

proof

thus (Seg ma) \ (Seg m1) c= (FinS (F,D)) " {x} :: according to XBOOLE_0:def 10 :: thesis: (FinS (F,D)) " {x} c= (Seg ma) \ (Seg m1)

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in (Seg ma) \ (Seg m1) or y in (FinS (F,D)) " {x} )
assume A18: y in (Seg ma) \ (Seg m1) ; :: thesis: y in (FinS (F,D)) " {x}
then reconsider l = y as Element of NAT ;
reconsider o = (FinS (F,D)) . l as Real ;
A19: y in Seg ma by A18, XBOOLE_0:def 5;
then A20: 1 <= l by FINSEQ_1:1;
A21: l <= ma by A19, FINSEQ_1:1;
then l <= len (FinS (F,D)) by A16, XXREAL_0:2;
then A22: l in dom (FinS (F,D)) by A20, FINSEQ_3:25;
not y in Seg m1 by A18, XBOOLE_0:def 5;
then ( l < 1 or m1 < l ) by FINSEQ_1:1;
then mi < l + 1 by A19, FINSEQ_1:1, XREAL_1:19;
then A23: mi <= l by NAT_1:13;

now :: thesis: ( ( l = ma & y in (FinS (F,D)) " {x} ) or ( l <> ma & y in (FinS (F,D)) " {x} ) )

per cases ( l = ma or l <> ma ) ;

case l = ma ; :: thesis: y in (FinS (F,D)) " {x}

then o in {x} by A11, TARSKI:def 1;
hence y in (FinS (F,D)) " {x} by A22, FUNCT_1:def 7; :: thesis: verum

end;

case l <> ma ; :: thesis: y in (FinS (F,D)) " {x}

then l < ma by A21, XXREAL_0:1;
then A24: o >= r by A11, A22, RFINSEQ:19;

now :: thesis: ( ( l = mi & y in (FinS (F,D)) " {x} ) or ( l <> mi & y in (FinS (F,D)) " {x} ) )

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

case l = mi ; :: thesis: y in (FinS (F,D)) " {x}

then o in {x} by A13, TARSKI:def 1;
hence y in (FinS (F,D)) " {x} by A22, FUNCT_1:def 7; :: thesis: verum

end;

case l <> mi ; :: thesis: y in (FinS (F,D)) " {x}

then mi < l by A23, XXREAL_0:1;
then r >= o by A13, A22, RFINSEQ:19;
then r = o by A24, XXREAL_0:1;
then o in {x} by TARSKI:def 1;
hence y in (FinS (F,D)) " {x} by A22, FUNCT_1:def 7; :: thesis: verum

end;

end;

end;

hence y in (FinS (F,D)) " {x} ; :: thesis: verum

end;

end;

end;

hence y in (FinS (F,D)) " {x} ; :: thesis: verum

end;

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in (FinS (F,D)) " {x} or y in (Seg ma) \ (Seg m1) )
assume A25: y in (FinS (F,D)) " {x} ; :: thesis: y in (Seg ma) \ (Seg m1)
then A26: y in dom (FinS (F,D)) by FUNCT_1:def 7;
reconsider l = y as Element of NAT by A25;
A27: 1 <= l by A26, FINSEQ_3:25;
(FinS (F,D)) . y in {x} by A25, FUNCT_1:def 7;
then A28: (FinS (F,D)) . l = x by TARSKI:def 1;
then mi <= l by A13, A26;
then mi < l + 1 by NAT_1:13;
then ( m1 < l or l < 1 ) by XREAL_1:19;
then A29: not l in Seg m1 by FINSEQ_1:1;
l <= ma by A11, A26, A28;
then l in Seg ma by A27, FINSEQ_1:1;
hence y in (Seg ma) \ (Seg m1) by A29, XBOOLE_0:def 5; :: thesis: verum

end;

A30: 1 <= ma by A11, FINSEQ_3:25;
A31: mi <= ma by A13, A11;
m1 <= mi by XREAL_1:43;
then A32: m1 <= ma by A31, XXREAL_0:2;
then Seg m1 c= Seg ma by FINSEQ_1:5;
then A33: card ((FinS (F,D)) " {x}) = (card (Seg ma)) - (card (Seg m1)) by A17, CARD_2:44
.= ma - (card (Seg m1)) by FINSEQ_1:57
.= ma - m1 by FINSEQ_1:57 ;
A34: mi <= len (FinS (F,D)) by A13, FINSEQ_3:25;
then 1 <= len (FinS (F,D)) by A14, XXREAL_0:2;
then A35: 1 in dom (FinS (F,D)) by FINSEQ_3:25;

now :: thesis: ( ( mi = 1 & card (p " {x}) = card ((FinS (F,D)) " {x}) ) or ( mi <> 1 & card (p " {x}) = card ((FinS (F,D)) " {x}) ) )

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

case A36: mi = 1 ; :: thesis: card (p " {x}) = card ((FinS (F,D)) " {x})

B . ma = p " {x}

proof

thus B . ma c= p " {x} :: according to XBOOLE_0:def 10 :: thesis: p " {x} c= B . ma

proof

defpred S₂[ Nat] means ( $1 in dom B & $1 <= ma implies for c being Element of C st c in B . $1 holds
c in p " {x} );
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in B . ma or y in p " {x} )
assume A37: y in B . ma ; :: thesis: y in p " {x}
B . ma c= C by A4, A1, A2, A11, Lm5;
then reconsider cy = y as Element of C by A37;
A38: for n being Nat st S₂[n] holds
S₂[n + 1]

proof

let n be Nat; :: thesis: ( S₂[n] implies S₂[n + 1] )
assume A39: S₂[n] ; :: thesis: S₂[n + 1]
assume that
A40: n + 1 in dom B and
A41: n + 1 <= ma ; :: thesis: for c being Element of C st c in B . (n + 1) holds
c in p " {x}
A42: n + 1 <= len B by A40, FINSEQ_3:25;
then A43: n <= (len B) - 1 by XREAL_1:19;
A44: n < len B by A42, NAT_1:13;
let c be Element of C; :: thesis: ( c in B . (n + 1) implies c in p " {x} )
assume A45: c in B . (n + 1) ; :: thesis: c in p " {x}
A46: n <= len B by A42, NAT_1:13;

now :: thesis: ( ( n = 0 & c in p " {x} ) or ( n <> 0 & c in p " {x} ) )

per cases ( n = 0 or n <> 0 ) ;

case n = 0 ; :: thesis: c in p " {x}

then p . c = x by A3, A13, A36, A45, Th14;
then p . c in {x} by TARSKI:def 1;
hence c in p " {x} by A5, FUNCT_1:def 7; :: thesis: verum

end;

case A47: n <> 0 ; :: thesis: c in p " {x}

then A48: 0 + 1 < n + 1 by XREAL_1:6;
A49: 0 + 1 <= n by A47, NAT_1:13;
then B . n c= B . (n + 1) by A43, Def2;
then A50: B . (n + 1) = (B . (n + 1)) \/ (B . n) by XBOOLE_1:12
.= ((B . (n + 1)) \ (B . n)) \/ (B . n) by XBOOLE_1:39 ;

now :: thesis: ( ( c in (B . (n + 1)) \ (B . n) & c in p " {x} ) or ( c in B . n & c in p " {x} ) )

per cases ( c in (B . (n + 1)) \ (B . n) or c in B . n ) by A45, A50, XBOOLE_0:def 3;

case c in (B . (n + 1)) \ (B . n) ; :: thesis: c in p " {x}

then A51: p . c = (FinS (F,D)) . (n + 1) by A3, A44, A49, Th14;

now :: thesis: ( ( n + 1 = ma & c in p " {x} ) or ( n + 1 <> ma & c in p " {x} ) )

per cases ( n + 1 = ma or n + 1 <> ma ) ;

case n + 1 = ma ; :: thesis: c in p " {x}

then p . c in {x} by A11, A51, TARSKI:def 1;
hence c in p " {x} by A5, FUNCT_1:def 7; :: thesis: verum

end;

case n + 1 <> ma ; :: thesis: c in p " {x}

then n + 1 < ma by A41, XXREAL_0:1;
then A52: p . c >= r by A4, A1, A2, A11, A40, A51, RFINSEQ:19;
r >= p . c by A4, A1, A2, A13, A36, A40, A48, A51, RFINSEQ:19;
then r = p . c by A52, XXREAL_0:1;
then p . c in {x} by TARSKI:def 1;
hence c in p " {x} by A5, FUNCT_1:def 7; :: thesis: verum

end;

end;

end;

hence c in p " {x} ; :: thesis: verum

end;

case c in B . n ; :: thesis: c in p " {x}

hence c in p " {x} by A39, A41, A46, A49, FINSEQ_3:25, NAT_1:13; :: thesis: verum

end;

end;

end;

hence c in p " {x} ; :: thesis: verum

end;

end;

end;

hence c in p " {x} ; :: thesis: verum

end;

A53: S₂[ 0 ] by FINSEQ_3:25;
A54: for n being Nat holds S₂[n] from NAT_1:sch 2(A53, A38);
ma in dom B by A4, A1, A11, FINSEQ_3:29;
then cy in p " {x} by A37, A54;
hence y in p " {x} ; :: thesis: verum

end;

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in p " {x} or y in B . ma )
assume A55: y in p " {x} ; :: thesis: y in B . ma
then reconsider cy = y as Element of C ;
p . cy in {x} by A55, FUNCT_1:def 7;
then A56: p . cy = x by TARSKI:def 1;
defpred S₂[ Nat] means ( $1 in dom B & ma < $1 & cy in B . $1 );
assume A57: not y in B . ma ; :: thesis: contradiction
A58: ex n being Nat st S₂[n]

proof

take n = len B; :: thesis: S₂[n]
len B <> 0 by Th4;
then 0 + 1 <= len B by NAT_1:13;
hence n in dom B by FINSEQ_3:25; :: thesis: ( ma < n & cy in B . n )
A59: B . n = C by Th3;

now :: thesis: not n <= ma

assume n <= ma ; :: thesis: contradiction
then ma = len B by A4, A1, A16, XXREAL_0:1;
then cy in B . ma by A59;
hence contradiction by A57; :: thesis: verum

end;

hence ( ma < n & cy in B . n ) by A59; :: thesis: verum

end;

consider mm being Nat such that
A60: ( S₂[mm] & ( for n being Nat st S₂[n] holds
mm <= n ) ) from NAT_1:sch 5(A58);
1 <= mm by A60, FINSEQ_3:25;
then max (0,(mm - 1)) = mm - 1 by FINSEQ_2:4;
then reconsider 1m = mm - 1 as Element of NAT by FINSEQ_2:5;
ma + 1 <= mm by A60, NAT_1:13;
then A61: ma <= 1m by XREAL_1:19;
then A62: 1 <= 1m by A30, XXREAL_0:2;
A63: mm in dom (FinS (F,D)) by A4, A1, A60, FINSEQ_3:29;
A64: mm <= len B by A60, FINSEQ_3:25;
A65: mm < mm + 1 by NAT_1:13;
then 1m < mm by XREAL_1:19;
then A66: 1m < len B by A64, XXREAL_0:2;
1m <= mm by A65, XREAL_1:19;
then 1m <= len B by A64, XXREAL_0:2;
then A67: 1m in dom B by A62, FINSEQ_3:25;

now :: thesis: ( ( ma = 1m & contradiction ) or ( ma <> 1m & contradiction ) )

per cases ( ma = 1m or ma <> 1m ) ;

case ma = 1m ; :: thesis: contradiction

then cy in (B . (1m + 1)) \ (B . 1m) by A57, A60, XBOOLE_0:def 5;
then p . cy = (FinS (F,D)) . mm by A3, A62, A66, Th14;
hence contradiction by A11, A56, A60, A63; :: thesis: verum

end;

case ma <> 1m ; :: thesis: contradiction

then A68: ma < 1m by A61, XXREAL_0:1;

now :: thesis: not cy in B . 1m

assume cy in B . 1m ; :: thesis: contradiction
then mm <= 1m by A60, A67, A68;
then mm - 1m <= 0 by XREAL_1:47;
hence contradiction ; :: thesis: verum

end;

then cy in (B . (1m + 1)) \ (B . 1m) by A60, XBOOLE_0:def 5;
then p . cy = (FinS (F,D)) . mm by A3, A62, A66, Th14;
hence contradiction by A11, A56, A60, A63; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

hence card (p " {x}) = card ((FinS (F,D)) " {x}) by A4, A1, A30, A16, A33, A36, Def1; :: thesis: verum

end;

case A69: mi <> 1 ; :: thesis: card (p " {x}) = card ((FinS (F,D)) " {x})

then 1 < mi by A14, XXREAL_0:1;
then A70: 1 <= m1 by A15, NAT_1:13;
A71: m1 <= len (FinS (F,D)) by A34, A15, NAT_1:13;
then A72: m1 in dom B by A4, A1, A70, FINSEQ_3:25;
then A73: B . m1 c= B . ma by A4, A1, A2, A11, A32, Th2;
B . ma c= C by A4, A1, A2, A11, Lm5;
then reconsider Bma = B . ma, Bm1 = B . m1 as finite set by A73;
(B . ma) \ (B . m1) = p " {x}

proof

thus (B . ma) \ (B . m1) c= p " {x} :: according to XBOOLE_0:def 10 :: thesis: p " {x} c= (B . ma) \ (B . m1)

proof

defpred S₂[ Nat] means ( $1 in dom B & mi <= $1 & $1 <= ma implies for c being Element of C st c in (B . $1) \ (B . m1) holds
c in p " {x} );
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in (B . ma) \ (B . m1) or y in p " {x} )
A74: B . ma c= C by A4, A1, A2, A11, Lm5;
A75: for n being Nat st S₂[n] holds
S₂[n + 1]

proof

let n be Nat; :: thesis: ( S₂[n] implies S₂[n + 1] )
assume A76: S₂[n] ; :: thesis: S₂[n + 1]
assume that
A77: n + 1 in dom B and
A78: mi <= n + 1 and
A79: n + 1 <= ma ; :: thesis: for c being Element of C st c in (B . (n + 1)) \ (B . m1) holds
c in p " {x}
let c be Element of C; :: thesis: ( c in (B . (n + 1)) \ (B . m1) implies c in p " {x} )
n + 1 <= len B by A77, FINSEQ_3:25;
then A80: n < len B by NAT_1:13;
assume A81: c in (B . (n + 1)) \ (B . m1) ; :: thesis: c in p " {x}

now :: thesis: ( ( n + 1 = mi & c in p " {x} ) or ( mi <> n + 1 & c in p " {x} ) )

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

case A82: n + 1 = mi ; :: thesis: c in p " {x}

then p . c = (FinS (F,D)) . (n + 1) by A3, A70, A80, A81, Th14;
then p . c in {x} by A13, A82, TARSKI:def 1;
hence c in p " {x} by A5, FUNCT_1:def 7; :: thesis: verum

end;

case mi <> n + 1 ; :: thesis: c in p " {x}

then A83: mi < n + 1 by A78, XXREAL_0:1;
then mi <= n by NAT_1:13;
then A84: 1 <= n by A14, XXREAL_0:2;
n <= ma by A79, NAT_1:13;
then A85: n <= len B by A4, A1, A16, XXREAL_0:2;
then ( n <= n + 1 & n in dom B ) by A84, FINSEQ_3:25, NAT_1:11;
then B . n c= B . (n + 1) by A77, Th2;
then A86: (B . (n + 1)) \ (B . m1) = ((B . (n + 1)) \/ (B . n)) \ (B . m1) by XBOOLE_1:12
.= (((B . (n + 1)) \ (B . n)) \/ (B . n)) \ (B . m1) by XBOOLE_1:39
.= (((B . (n + 1)) \ (B . n)) \ (B . m1)) \/ ((B . n) \ (B . m1)) by XBOOLE_1:42 ;

now :: thesis: ( ( c in ((B . (n + 1)) \ (B . n)) \ (B . m1) & c in p " {x} ) or ( c in (B . n) \ (B . m1) & c in p " {x} ) )

per cases ( c in ((B . (n + 1)) \ (B . n)) \ (B . m1) or c in (B . n) \ (B . m1) ) by A81, A86, XBOOLE_0:def 3;

case c in ((B . (n + 1)) \ (B . n)) \ (B . m1) ; :: thesis: c in p " {x}

then c in (B . (n + 1)) \ (B . n) by XBOOLE_0:def 5;
then A87: p . c = (FinS (F,D)) . (n + 1) by A3, A80, A84, Th14;

now :: thesis: ( ( n + 1 = ma & c in p " {x} ) or ( n + 1 <> ma & c in p " {x} ) )

per cases ( n + 1 = ma or n + 1 <> ma ) ;

case n + 1 = ma ; :: thesis: c in p " {x}

then p . c in {x} by A11, A87, TARSKI:def 1;
hence c in p " {x} by A5, FUNCT_1:def 7; :: thesis: verum

end;

case n + 1 <> ma ; :: thesis: c in p " {x}

then n + 1 < ma by A79, XXREAL_0:1;
then A88: p . c >= r by A4, A1, A2, A11, A77, A87, RFINSEQ:19;
r >= p . c by A4, A1, A2, A13, A77, A83, A87, RFINSEQ:19;
then r = p . c by A88, XXREAL_0:1;
then p . c in {x} by TARSKI:def 1;
hence c in p " {x} by A5, FUNCT_1:def 7; :: thesis: verum

end;

end;

end;

hence c in p " {x} ; :: thesis: verum

end;

case c in (B . n) \ (B . m1) ; :: thesis: c in p " {x}

hence c in p " {x} by A76, A79, A83, A84, A85, FINSEQ_3:25, NAT_1:13; :: thesis: verum

end;

end;

end;

hence c in p " {x} ; :: thesis: verum

end;

end;

end;

hence c in p " {x} ; :: thesis: verum

end;

A89: S₂[ 0 ] ;
A90: for n being Nat holds S₂[n] from NAT_1:sch 2(A89, A75);
assume A91: y in (B . ma) \ (B . m1) ; :: thesis: y in p " {x}
then y in B . ma ;
then reconsider cy = y as Element of C by A74;
ma in dom B by A4, A1, A11, FINSEQ_3:29;
then cy in p " {x} by A31, A91, A90;
hence y in p " {x} ; :: thesis: verum

end;

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in p " {x} or y in (B . ma) \ (B . m1) )
assume A92: y in p " {x} ; :: thesis: y in (B . ma) \ (B . m1)
then reconsider cy = y as Element of C ;
p . cy in {x} by A92, FUNCT_1:def 7;
then A93: p . cy = x by TARSKI:def 1;
assume A94: not y in (B . ma) \ (B . m1) ; :: thesis: contradiction

now :: thesis: ( ( not y in B . ma & contradiction ) or ( y in B . m1 & contradiction ) )

per cases ( not y in B . ma or y in B . m1 ) by A94, XBOOLE_0:def 5;

case A95: not y in B . ma ; :: thesis: contradiction

defpred S₂[ Nat] means ( $1 in dom B & ma < $1 & cy in B . $1 );
A96: ex n being Nat st S₂[n]

proof

take n = len B; :: thesis: S₂[n]
len B <> 0 by Th4;
then 0 + 1 <= len B by NAT_1:13;
hence n in dom B by FINSEQ_3:25; :: thesis: ( ma < n & cy in B . n )
A97: B . n = C by Th3;

now :: thesis: not n <= ma

assume n <= ma ; :: thesis: contradiction
then ma = len B by A4, A1, A16, XXREAL_0:1;
then cy in B . ma by A97;
hence contradiction by A95; :: thesis: verum

end;

hence ( ma < n & cy in B . n ) by A97; :: thesis: verum

end;

consider mm being Nat such that
A98: ( S₂[mm] & ( for n being Nat st S₂[n] holds
mm <= n ) ) from NAT_1:sch 5(A96);
1 <= mm by A98, FINSEQ_3:25;
then max (0,(mm - 1)) = mm - 1 by FINSEQ_2:4;
then reconsider 1m = mm - 1 as Element of NAT by FINSEQ_2:5;
ma + 1 <= mm by A98, NAT_1:13;
then A99: ma <= 1m by XREAL_1:19;
then A100: 1 <= 1m by A30, XXREAL_0:2;
A101: mm in dom (FinS (F,D)) by A4, A1, A98, FINSEQ_3:29;
A102: mm <= len B by A98, FINSEQ_3:25;
A103: mm < mm + 1 by NAT_1:13;
then 1m < mm by XREAL_1:19;
then A104: 1m < len B by A102, XXREAL_0:2;
1m <= mm by A103, XREAL_1:19;
then 1m <= len B by A102, XXREAL_0:2;
then A105: 1m in dom B by A100, FINSEQ_3:25;

now :: thesis: ( ( ma = 1m & contradiction ) or ( ma <> 1m & contradiction ) )

per cases ( ma = 1m or ma <> 1m ) ;

case ma = 1m ; :: thesis: contradiction

then cy in (B . (1m + 1)) \ (B . 1m) by A95, A98, XBOOLE_0:def 5;
then p . cy = (FinS (F,D)) . mm by A3, A100, A104, Th14;
hence contradiction by A11, A93, A98, A101; :: thesis: verum

end;

case ma <> 1m ; :: thesis: contradiction

then A106: ma < 1m by A99, XXREAL_0:1;

now :: thesis: not cy in B . 1m

assume cy in B . 1m ; :: thesis: contradiction
then mm <= 1m by A98, A105, A106;
then mm - 1m <= 0 by XREAL_1:47;
hence contradiction ; :: thesis: verum

end;

then cy in (B . (1m + 1)) \ (B . 1m) by A98, XBOOLE_0:def 5;
then p . cy = (FinS (F,D)) . mm by A3, A100, A104, Th14;
hence contradiction by A11, A93, A98, A101; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

case A107: y in B . m1 ; :: thesis: contradiction

defpred S₂[ Nat] means ( $1 in dom B & $1 <= m1 & cy in B . $1 );
A108: ex n being Nat st S₂[n] by A72, A107;
consider mm being Nat such that
A109: ( S₂[mm] & ( for n being Nat st S₂[n] holds
mm <= n ) ) from NAT_1:sch 5(A108);
A110: 1 <= mm by A109, FINSEQ_3:25;
then max (0,(mm - 1)) = mm - 1 by FINSEQ_2:4;
then reconsider 1m = mm - 1 as Element of NAT by FINSEQ_2:5;
A111: mm <= len B by A109, FINSEQ_3:25;
A112: mm in dom (FinS (F,D)) by A4, A1, A109, FINSEQ_3:29;

now :: thesis: ( ( mm = 1 & contradiction ) or ( mm <> 1 & contradiction ) )

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

case mm = 1 ; :: thesis: contradiction

then p . cy = (FinS (F,D)) . 1 by A3, A109, Th14;
then mi <= 1 by A13, A35, A93;
hence contradiction by A14, A69, XXREAL_0:1; :: thesis: verum

end;

case mm <> 1 ; :: thesis: contradiction

then 1 < mm by A110, XXREAL_0:1;
then 1 + 1 <= mm by NAT_1:13;
then A113: 1 <= 1m by XREAL_1:19;
A114: mm < mm + 1 by NAT_1:13;
then A115: 1m <= mm by XREAL_1:19;
then 1m <= len B by A111, XXREAL_0:2;
then A116: 1m in dom B by A113, FINSEQ_3:25;
A117: 1m < mm by A114, XREAL_1:19;
then A118: 1m < len B by A111, XXREAL_0:2;
1m <= m1 by A109, A115, XXREAL_0:2;
then not cy in B . 1m by A109, A117, A116;
then cy in (B . (1m + 1)) \ (B . 1m) by A109, XBOOLE_0:def 5;
then p . cy = (FinS (F,D)) . (1m + 1) by A3, A113, A118, Th14;
then mi <= mm by A13, A93, A112;
then m1 + 1 <= m1 by A109, XXREAL_0:2;
then 1 <= m1 - m1 by XREAL_1:19;
then 1 <= 0 ;
hence contradiction ; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

hence card (p " {x}) = (card Bma) - (card Bm1) by A73, CARD_2:44
.= ma - (card Bm1) by A4, A1, A30, A16, Def1
.= card ((FinS (F,D)) " {x}) by A4, A1, A33, A70, A71, Def1 ;
:: thesis: verum

end;

end;

end;

hence card ((FinS (F,D)) " {x}) = card (p " {x}) ; :: thesis: verum

end;

end;

end;

hence card (Coim ((FinS (F,D)),x)) = card (Coim (p,x)) ; :: thesis: verum

end;

hence Rland (F,B), FinS (F,D) are_fiberwise_equipotent by CLASSES1:def 10; :: thesis: verum