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
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:29;
assume A1: ( F is total & card C = card D ) ; :: thesis: Rland F,B, FinS F,D are_fiberwise_equipotent
then A2: rng p = rng (FinS F,D) by Th16;
A3: ( 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;
A4: ( dom p = C & dom F = D ) by A1, Th13, PARTFUN1:def 4;
A5: ( dom (FinS F,D) = Seg (len (FinS F,D)) & dom B = Seg (len B) ) by FINSEQ_1:def 3;

now

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

now

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

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

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

end;

case A6: 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 );
A7: ex n being Nat st S₁[n] by A6, FINSEQ_2:11;
A8: ex n being Nat st S₁[n] by A6, FINSEQ_2:11;
A9: for n being Nat st S₁[n] holds
n <= len (FinS F,D) by FINSEQ_3:27;
consider mi being Nat such that
A10: ( S₁[mi] & ( for n being Nat st S₁[n] holds
mi <= n ) ) from NAT_1:sch 5(A8);
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, A7);
A12: mi <= ma by A10, A11;
A13: ( 1 <= mi & mi <= len (FinS F,D) & 1 <= ma & ma <= len (FinS F,D) ) by A10, A11, 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;
reconsider r = x as Real by A10;
1 <= len (FinS F,D) by A13, XXREAL_0:2;
then A14: 1 in dom (FinS F,D) by FINSEQ_3:27;
m1 <= mi by XREAL_1:45;
then A15: ( m1 <= ma & m1 + 1 = mi ) by A12, XXREAL_0:2;
then A16: ( Seg m1 c= Seg ma & Seg ma is finite ) by FINSEQ_1:7;
(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 set ; :: according to TARSKI:def 3 :: thesis: ( not y in (Seg ma) \ (Seg m1) or y in (FinS F,D) " {x} )
assume A17: y in (Seg ma) \ (Seg m1) ; :: thesis: y in (FinS F,D) " {x}
then A18: ( y in Seg ma & not y in Seg m1 & Seg ma c= NAT ) by XBOOLE_0:def 5;
reconsider l = y as Element of NAT by A17;
A19: ( 1 <= l & l <= ma & ( l < 1 or m1 < l ) ) by A18, FINSEQ_1:3;
then mi < l + 1 by XREAL_1:21;
then A20: mi <= l by NAT_1:13;
l <= len (FinS F,D) by A13, A19, XXREAL_0:2;
then A21: l in dom (FinS F,D) by A19, FINSEQ_3:27;
reconsider o = (FinS F,D) . l as Real ;

now

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 A21, FUNCT_1:def 13; :: thesis: verum

end;

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

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

now

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

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

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

end;

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

then mi < l by A20, XXREAL_0:1;
then r >= o by A10, A21, RFINSEQ:32;
then r = o by A22, XXREAL_0:1;
then o in {x} by TARSKI:def 1;
hence y in (FinS F,D) " {x} by A21, FUNCT_1:def 13; :: 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 set ; :: according to TARSKI:def 3 :: thesis: ( not y in (FinS F,D) " {x} or y in (Seg ma) \ (Seg m1) )
assume A23: y in (FinS F,D) " {x} ; :: thesis: y in (Seg ma) \ (Seg m1)
then A24: ( y in dom (FinS F,D) & (FinS F,D) . y in {x} ) by FUNCT_1:def 13;
reconsider l = y as Element of NAT by A23;
A25: (FinS F,D) . l = x by A24, TARSKI:def 1;
then mi <= l by A10, A24;
then mi < l + 1 by NAT_1:13;
then ( m1 < l or l < 1 ) by XREAL_1:21;
then A26: not l in Seg m1 by FINSEQ_1:3;
( 1 <= l & l <= ma ) by A11, A24, A25, FINSEQ_3:27;
then l in Seg ma by FINSEQ_1:3;
hence y in (Seg ma) \ (Seg m1) by A26, XBOOLE_0:def 5; :: thesis: verum

end;

then A27: card ((FinS F,D) " {x}) = (card (Seg ma)) - (card (Seg m1)) by A16, CARD_2:63
.= ma - (card (Seg m1)) by FINSEQ_1:78
.= ma - m1 by FINSEQ_1:78 ;

now

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

case A28: 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

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in B . ma or y in p " {x} )
assume A29: y in B . ma ; :: thesis: y in p " {x}
B . ma c= C by A3, A5, A11, Lm5;
then reconsider cy = y as Element of C by A29;
defpred S₂[ Element of 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} );
A30: S₂[ 0 ] by FINSEQ_3:27;
A31: for n being Element of NAT st S₂[n] holds
S₂[n + 1]

proof

let n be Element of NAT ; :: thesis: ( S₂[n] implies S₂[n + 1] )
assume A32: S₂[n] ; :: thesis: S₂[n + 1]
assume A33: ( n + 1 in dom B & n + 1 <= ma ) ; :: thesis: for c being Element of C st c in B . (n + 1) holds
c in p " {x}
then ( 1 <= n + 1 & n + 1 <= len B & n <= n + 1 ) by FINSEQ_3:27, NAT_1:11;
then A34: ( n <= len B & n <= ma & n <= (len B) - 1 & n < len B ) by A33, NAT_1:13, XREAL_1:21;
let c be Element of C; :: thesis: ( c in B . (n + 1) implies c in p " {x} )
assume A35: c in B . (n + 1) ; :: thesis: c in p " {x}

now

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

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

then p . c = x by A1, A10, A28, A35, Th15;
then p . c in {x} by TARSKI:def 1;
hence c in p " {x} by A4, FUNCT_1:def 13; :: thesis: verum

end;

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

then 0 < n ;
then A36: ( 0 + 1 <= n & 0 + 1 < n + 1 ) by NAT_1:13, XREAL_1:8;
then B . n c= B . (n + 1) by A34, Def2;
then A37: B . (n + 1) = (B . (n + 1)) \/ (B . n) by XBOOLE_1:12
.= ((B . (n + 1)) \ (B . n)) \/ (B . n) by XBOOLE_1:39 ;

now

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

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

then A38: p . c = (FinS F,D) . (n + 1) by A1, A34, A36, Th15;

now

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, A38, TARSKI:def 1;
hence c in p " {x} by A4, FUNCT_1:def 13; :: thesis: verum

end;

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

then n + 1 < ma by A33, XXREAL_0:1;
then A39: p . c >= r by A3, A5, A11, A33, A38, RFINSEQ:32;
r >= p . c by A3, A5, A10, A28, A33, A36, A38, RFINSEQ:32;
then r = p . c by A39, XXREAL_0:1;
then p . c in {x} by TARSKI:def 1;
hence c in p " {x} by A4, FUNCT_1:def 13; :: 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 A32, A34, A36, FINSEQ_3:27; :: thesis: verum

end;

end;

end;

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

end;

end;

end;

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

end;

A40: ma in dom B by A3, A11, FINSEQ_3:31;
for n being Element of NAT holds S₂[n] from NAT_1:sch 1(A30, A31);
then cy in p " {x} by A29, A40;
hence y in p " {x} ; :: thesis: verum

end;

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

proof

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

now

assume n <= ma ; :: thesis: contradiction
then ma = len B by A3, A13, XXREAL_0:1;
then cy in B . ma by A45;
hence contradiction by A42; :: thesis: verum

end;

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

end;

consider mm being Nat such that
A46: ( S₂[mm] & ( for n being Nat st S₂[n] holds
mm <= n ) ) from NAT_1:sch 5(A44);
1 <= mm by A46, FINSEQ_3:27;
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 & mm <= mm + 1 & mm < mm + 1 ) by A46, NAT_1:13;
then A47: ( ma <= 1m & mm <= len B & 1m <= mm & 1m < mm ) by A46, FINSEQ_3:27, XREAL_1:21;
then A48: ( 1 <= 1m & 1m <= len B & 1m < len B ) by A13, XXREAL_0:2;
then A49: ( 1m in dom B & 1m + 1 <= len B ) by FINSEQ_3:27, NAT_1:13;
A50: mm in dom (FinS F,D) by A3, A46, FINSEQ_3:31;

now

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

case ma = 1m ; :: thesis: contradiction

then cy in (B . (1m + 1)) \ (B . 1m) by A42, A46, XBOOLE_0:def 5;
then p . cy = (FinS F,D) . mm by A1, A48, Th15;
hence contradiction by A11, A43, A46, A50; :: thesis: verum

end;

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

then A51: ma < 1m by A47, XXREAL_0:1;

now

assume cy in B . 1m ; :: thesis: contradiction
then mm <= 1m by A46, A49, A51;
then mm - 1m <= 0 by XREAL_1:49;
hence contradiction ; :: thesis: verum

end;

then cy in (B . (1m + 1)) \ (B . 1m) by A46, XBOOLE_0:def 5;
then p . cy = (FinS F,D) . mm by A1, A48, Th15;
hence contradiction by A11, A43, A46, A50; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

hence card (p " {x}) = card ((FinS F,D) " {x}) by A3, A13, A27, A28, Def1; :: thesis: verum

end;

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

then 1 < mi by A13, XXREAL_0:1;
then A53: ( 1 <= m1 & m1 <= len (FinS F,D) ) by A13, A15, NAT_1:13;
then A54: m1 in dom B by A3, FINSEQ_3:27;
then A55: B . m1 c= B . ma by A3, A5, A11, A15, Th2;
B . ma c= C by A3, A5, A11, Lm5;
then B . ma is finite ;
then reconsider Bma = B . ma, Bm1 = B . m1 as finite set by A55;
(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

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in (B . ma) \ (B . m1) or y in p " {x} )
assume A56: y in (B . ma) \ (B . m1) ; :: thesis: y in p " {x}
then A57: ( y in B . ma & not y in B . m1 ) by XBOOLE_0:def 5;
B . ma c= C by A3, A5, A11, Lm5;
then reconsider cy = y as Element of C by A57;
defpred S₂[ Element of 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} );
A58: S₂[ 0 ] ;
A59: for n being Element of NAT st S₂[n] holds
S₂[n + 1]

proof

let n be Element of NAT ; :: thesis: ( S₂[n] implies S₂[n + 1] )
assume A60: S₂[n] ; :: thesis: S₂[n + 1]
assume A61: ( n + 1 in dom B & mi <= n + 1 & n + 1 <= ma ) ; :: thesis: for c being Element of C st c in (B . (n + 1)) \ (B . m1) holds
c in p " {x}
then ( 1 <= n + 1 & n + 1 <= len B & n <= n + 1 ) by FINSEQ_3:27, NAT_1:11;
then A62: ( n <= len B & n <= ma & n <= (len B) - 1 & n < len B ) by A61, NAT_1:13, XREAL_1:21;
let c be Element of C; :: thesis: ( c in (B . (n + 1)) \ (B . m1) implies c in p " {x} )
assume A63: c in (B . (n + 1)) \ (B . m1) ; :: thesis: c in p " {x}

now

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

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

then p . c = (FinS F,D) . (n + 1) by A1, A53, A62, A63, Th15;
then p . c in {x} by A10, A64, TARSKI:def 1;
hence c in p " {x} by A4, FUNCT_1:def 13; :: thesis: verum

end;

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

then A65: ( mi < n + 1 & n <= n + 1 ) by A61, NAT_1:11, XXREAL_0:1;
then ( mi <= n & n <= ma ) by A61, NAT_1:13;
then A66: ( 1 <= n & n <= len B ) by A3, A13, XXREAL_0:2;
then n in dom B by FINSEQ_3:27;
then B . n c= B . (n + 1) by A61, A65, Th2;
then A67: (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

per cases ( c in ((B . (n + 1)) \ (B . n)) \ (B . m1) or c in (B . n) \ (B . m1) ) by A63, A67, 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 A68: p . c = (FinS F,D) . (n + 1) by A1, A62, A66, Th15;

now

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, A68, TARSKI:def 1;
hence c in p " {x} by A4, FUNCT_1:def 13; :: thesis: verum

end;

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

then n + 1 < ma by A61, XXREAL_0:1;
then A69: p . c >= r by A3, A5, A11, A61, A68, RFINSEQ:32;
r >= p . c by A3, A5, A10, A61, A65, A68, RFINSEQ:32;
then r = p . c by A69, XXREAL_0:1;
then p . c in {x} by TARSKI:def 1;
hence c in p " {x} by A4, FUNCT_1:def 13; :: 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 A60, A61, A65, A66, FINSEQ_3:27, 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;

A70: ma in dom B by A3, A11, FINSEQ_3:31;
for n being Element of NAT holds S₂[n] from NAT_1:sch 1(A58, A59);
then cy in p " {x} by A12, A56, A70;
hence y in p " {x} ; :: thesis: verum

end;

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in p " {x} or y in (B . ma) \ (B . m1) )
assume A71: y in p " {x} ; :: thesis: y in (B . ma) \ (B . m1)
then reconsider cy = y as Element of C ;
( cy in dom p & p . cy in {x} ) by A71, FUNCT_1:def 13;
then A72: p . cy = x by TARSKI:def 1;
assume A73: not y in (B . ma) \ (B . m1) ; :: thesis: contradiction

now

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

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

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

proof

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

now

assume n <= ma ; :: thesis: contradiction
then ma = len B by A3, A13, XXREAL_0:1;
then cy in B . ma by A76;
hence contradiction by A74; :: thesis: verum

end;

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

end;

consider mm being Nat such that
A77: ( S₂[mm] & ( for n being Nat st S₂[n] holds
mm <= n ) ) from NAT_1:sch 5(A75);
1 <= mm by A77, FINSEQ_3:27;
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 & mm <= mm + 1 & mm < mm + 1 ) by A77, NAT_1:13;
then A78: ( ma <= 1m & mm <= len B & 1m <= mm & 1m < mm ) by A77, FINSEQ_3:27, XREAL_1:21;
then A79: ( 1 <= 1m & 1m <= len B & 1m < len B ) by A13, XXREAL_0:2;
then A80: ( 1m in dom B & 1m + 1 <= len B ) by FINSEQ_3:27, NAT_1:13;
A81: mm in dom (FinS F,D) by A3, A77, FINSEQ_3:31;

now

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

case ma = 1m ; :: thesis: contradiction

then cy in (B . (1m + 1)) \ (B . 1m) by A74, A77, XBOOLE_0:def 5;
then p . cy = (FinS F,D) . mm by A1, A79, Th15;
hence contradiction by A11, A72, A77, A81; :: thesis: verum

end;

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

then A82: ma < 1m by A78, XXREAL_0:1;

now

assume cy in B . 1m ; :: thesis: contradiction
then mm <= 1m by A77, A80, A82;
then mm - 1m <= 0 by XREAL_1:49;
hence contradiction ; :: thesis: verum

end;

then cy in (B . (1m + 1)) \ (B . 1m) by A77, XBOOLE_0:def 5;
then p . cy = (FinS F,D) . mm by A1, A79, Th15;
hence contradiction by A11, A72, A77, A81; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

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

defpred S₂[ Nat] means ( $1 in dom B & $1 <= m1 & cy in B . $1 );
A84: ex n being Nat st S₂[n] by A54, A83;
consider mm being Nat such that
A85: ( S₂[mm] & ( for n being Nat st S₂[n] holds
mm <= n ) ) from NAT_1:sch 5(A84);
A86: ( 1 <= mm & mm <= len B ) by A85, FINSEQ_3:27;
then max 0 ,(mm - 1) = mm - 1 by FINSEQ_2:4;
then reconsider 1m = mm - 1 as Element of NAT by FINSEQ_2:5;
A87: mm in dom (FinS F,D) by A3, A85, FINSEQ_3:31;

now

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

case mm = 1 ; :: thesis: contradiction

then p . cy = (FinS F,D) . 1 by A1, A85, Th15;
then mi <= 1 by A10, A14, A72;
hence contradiction by A13, A52, XXREAL_0:1; :: thesis: verum

end;

case mm <> 1 ; :: thesis: contradiction

then ( 1 < mm & mm <= mm + 1 & mm < mm + 1 ) by A86, NAT_1:13, XXREAL_0:1;
then A88: ( 1 + 1 <= mm & 1m <= mm & 1m < mm ) by NAT_1:13, XREAL_1:21;
then A89: ( 1 <= 1m & 1m <= len B & 1m < len B & 1m <= m1 ) by A85, A86, XREAL_1:21, XXREAL_0:2;
then 1m in dom B by FINSEQ_3:27;
then not cy in B . 1m by A85, A88, A89;
then cy in (B . (1m + 1)) \ (B . 1m) by A85, XBOOLE_0:def 5;
then p . cy = (FinS F,D) . (1m + 1) by A1, A89, Th15;
then mi <= mm by A10, A72, A87;
then m1 + 1 <= m1 by A85, XXREAL_0:2;
then 1 <= m1 - m1 by XREAL_1:21;
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 A55, CARD_2:63
.= ma - (card Bm1) by A3, A13, Def1
.= card ((FinS F,D) " {x}) by A3, A27, A53, 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 9; :: thesis: verum