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
Rlor 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
Rlor F,A, FinS F,D are_fiberwise_equipotent
let B be RearrangmentGen of C; :: thesis: ( F is total & card C = card D implies Rlor F,B, FinS F,D are_fiberwise_equipotent )
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;
assume A1: ( F is total & card C = card D ) ; :: thesis: Rlor F,B, FinS F,D are_fiberwise_equipotent
then A2: rng (Rlor F,B) = rng (FinS F,D) by Th23;
A3: ( len (MIM (FinS F,D)) = len (CHI (Co_Gen B),C) & len (CHI (Co_Gen B),C) = len (Co_Gen B) & len (MIM (FinS F,D)) = len (FinS F,D) ) by A1, Th12, RFINSEQ:def 3, RFUNCT_3:def 6;
A4: ( dom (Rlor F,B) = C & dom F = D ) by A1, Th21, PARTFUN1:def 4;
then reconsider p = Rlor F,B as finite PartFunc of C,REAL by FINSET_1:29;
A5: ( dom (FinS F,D) = Seg (len (FinS F,D)) & dom (Co_Gen B) = Seg (len (Co_Gen 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: for n being Nat st S₁[n] holds
n <= len (FinS F,D) by FINSEQ_3:27;
consider mi being Nat such that
A9: ( S₁[mi] & ( for n being Nat st S₁[n] holds
mi <= n ) ) from NAT_1:sch 5(A7);
consider ma being Nat such that
A10: ( S₁[ma] & ( for n being Nat st S₁[n] holds
n <= ma ) ) from NAT_1:sch 6(A8, A7);
A11: mi <= ma by A9, A10;
A12: ( 1 <= mi & mi <= len (FinS F,D) & 1 <= ma & ma <= len (FinS F,D) ) by A9, A10, 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 A9;
1 <= len (FinS F,D) by A12, XXREAL_0:2;
then A13: 1 in dom (FinS F,D) by FINSEQ_3:27;
m1 <= mi by XREAL_1:45;
then A14: ( m1 <= ma & m1 + 1 = mi ) by A11, XXREAL_0:2;
then A15: ( 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 A16: y in (Seg ma) \ (Seg m1) ; :: thesis: y in (FinS F,D) " {x}
then A17: ( 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 A16;
A18: ( 1 <= l & l <= ma & ( l < 1 or m1 < l ) ) by A17, FINSEQ_1:3;
then mi < l + 1 by XREAL_1:21;
then A19: mi <= l by NAT_1:13;
l <= len (FinS F,D) by A12, A18, XXREAL_0:2;
then A20: l in dom (FinS F,D) by A18, 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 A10, TARSKI:def 1;
hence y in (FinS F,D) " {x} by A20, FUNCT_1:def 13; :: thesis: verum

end;

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

then l < ma by A18, XXREAL_0:1;
then A21: o >= r by A10, A20, 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 A9, TARSKI:def 1;
hence y in (FinS F,D) " {x} by A20, FUNCT_1:def 13; :: thesis: verum

end;

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

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

end;

then A26: card ((FinS F,D) " {x}) = (card (Seg ma)) - (card (Seg m1)) by A15, 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 A27: mi = 1 ; :: thesis: card (p " {x}) = card ((FinS F,D) " {x})

(Co_Gen B) . ma = p " {x}

proof

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

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in (Co_Gen B) . ma or y in p " {x} )
assume A28: y in (Co_Gen B) . ma ; :: thesis: y in p " {x}
(Co_Gen B) . ma c= C by A3, A5, A10, Lm5;
then reconsider cy = y as Element of C by A28;
defpred S₂[ Element of NAT ] means ( $1 in dom (Co_Gen B) & $1 <= ma implies for c being Element of C st c in (Co_Gen B) . $1 holds
c in p " {x} );
A29: S₂[ 0 ] by FINSEQ_3:27;
A30: 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 A31: S₂[n] ; :: thesis: S₂[n + 1]
assume A32: ( n + 1 in dom (Co_Gen B) & n + 1 <= ma ) ; :: thesis: for c being Element of C st c in (Co_Gen B) . (n + 1) holds
c in p " {x}
then ( 1 <= n + 1 & n + 1 <= len (Co_Gen B) & n <= n + 1 ) by FINSEQ_3:27, NAT_1:11;
then A33: ( n <= len (Co_Gen B) & n <= ma & n <= (len (Co_Gen B)) - 1 & n < len (Co_Gen B) ) by A32, NAT_1:13, XREAL_1:21;
let c be Element of C; :: thesis: ( c in (Co_Gen B) . (n + 1) implies c in p " {x} )
assume A34: c in (Co_Gen 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, A9, A27, A34, Th22;
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 A35: ( 0 + 1 <= n & 0 + 1 < n + 1 ) by NAT_1:13, XREAL_1:8;
then (Co_Gen B) . n c= (Co_Gen B) . (n + 1) by A33, Def2;
then A36: (Co_Gen B) . (n + 1) = ((Co_Gen B) . (n + 1)) \/ ((Co_Gen B) . n) by XBOOLE_1:12
.= (((Co_Gen B) . (n + 1)) \ ((Co_Gen B) . n)) \/ ((Co_Gen B) . n) by XBOOLE_1:39 ;

now

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

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

then A37: p . c = (FinS F,D) . (n + 1) by A1, A33, A35, Th22;

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 A10, A37, 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 A32, XXREAL_0:1;
then A38: p . c >= r by A3, A5, A10, A32, A37, RFINSEQ:32;
r >= p . c by A3, A5, A9, A27, A32, A35, A37, RFINSEQ:32;
then r = p . c by A38, 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 (Co_Gen B) . n ; :: thesis: c in p " {x}

hence c in p " {x} by A31, A33, A35, 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;

A39: ma in dom (Co_Gen B) by A3, A10, FINSEQ_3:31;
for n being Element of NAT holds S₂[n] from NAT_1:sch 1(A29, A30);
then cy in p " {x} by A28, A39;
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 (Co_Gen B) . ma )
assume A40: y in p " {x} ; :: thesis: y in (Co_Gen B) . ma
then reconsider cy = y as Element of C ;
assume A41: not y in (Co_Gen B) . ma ; :: thesis: contradiction
( cy in dom p & p . cy in {x} ) by A40, FUNCT_1:def 13;
then A42: p . cy = x by TARSKI:def 1;
defpred S₂[ Nat] means ( $1 in dom (Co_Gen B) & ma < $1 & cy in (Co_Gen B) . $1 );
A43: ex n being Nat st S₂[n]

proof

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

now

assume n <= ma ; :: thesis: contradiction
then ma = len (Co_Gen B) by A3, A12, XXREAL_0:1;
then cy in (Co_Gen B) . ma by A44;
hence contradiction by A41; :: thesis: verum

end;

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

end;

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

now

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

case ma = 1m ; :: thesis: contradiction

then cy in ((Co_Gen B) . (1m + 1)) \ ((Co_Gen B) . 1m) by A41, A45, XBOOLE_0:def 5;
then p . cy = (FinS F,D) . mm by A1, A47, Th22;
hence contradiction by A10, A42, A45, A49; :: thesis: verum

end;

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

then A50: ma < 1m by A46, XXREAL_0:1;

now

assume cy in (Co_Gen B) . 1m ; :: thesis: contradiction
then mm <= 1m by A45, A48, A50;
then mm - 1m <= 0 by XREAL_1:49;
hence contradiction ; :: thesis: verum

end;

then cy in ((Co_Gen B) . (1m + 1)) \ ((Co_Gen B) . 1m) by A45, XBOOLE_0:def 5;
then p . cy = (FinS F,D) . mm by A1, A47, Th22;
hence contradiction by A10, A42, A45, A49; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

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

end;

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

then 1 < mi by A12, XXREAL_0:1;
then A52: ( 1 <= m1 & m1 <= len (FinS F,D) ) by A12, A14, NAT_1:13;
then A53: m1 in dom (Co_Gen B) by A3, FINSEQ_3:27;
then A54: (Co_Gen B) . m1 c= (Co_Gen B) . ma by A3, A5, A10, A14, Th2;
(Co_Gen B) . ma c= C by A3, A5, A10, Lm5;
then (Co_Gen B) . ma is finite ;
then reconsider bma = (Co_Gen B) . ma, bm1 = (Co_Gen B) . m1 as finite set by A54;
((Co_Gen B) . ma) \ ((Co_Gen B) . m1) = p " {x}

proof

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

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in ((Co_Gen B) . ma) \ ((Co_Gen B) . m1) or y in p " {x} )
assume A55: y in ((Co_Gen B) . ma) \ ((Co_Gen B) . m1) ; :: thesis: y in p " {x}
then A56: ( y in (Co_Gen B) . ma & not y in (Co_Gen B) . m1 ) by XBOOLE_0:def 5;
(Co_Gen B) . ma c= C by A3, A5, A10, Lm5;
then reconsider cy = y as Element of C by A56;
defpred S₂[ Element of NAT ] means ( $1 in dom (Co_Gen B) & mi <= $1 & $1 <= ma implies for c being Element of C st c in ((Co_Gen B) . $1) \ ((Co_Gen B) . m1) holds
c in p " {x} );
A57: S₂[ 0 ] ;
A58: 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 A59: S₂[n] ; :: thesis: S₂[n + 1]
assume A60: ( n + 1 in dom (Co_Gen B) & mi <= n + 1 & n + 1 <= ma ) ; :: thesis: for c being Element of C st c in ((Co_Gen B) . (n + 1)) \ ((Co_Gen B) . m1) holds
c in p " {x}
then ( 1 <= n + 1 & n + 1 <= len (Co_Gen B) & n <= n + 1 ) by FINSEQ_3:27, NAT_1:11;
then A61: ( n <= len (Co_Gen B) & n <= ma & n <= (len (Co_Gen B)) - 1 & n < len (Co_Gen B) ) by A60, NAT_1:13, XREAL_1:21;
let c be Element of C; :: thesis: ( c in ((Co_Gen B) . (n + 1)) \ ((Co_Gen B) . m1) implies c in p " {x} )
assume A62: c in ((Co_Gen B) . (n + 1)) \ ((Co_Gen B) . m1) ; :: thesis: c in p " {x}

now

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

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

then p . c = (FinS F,D) . (n + 1) by A1, A52, A61, A62, Th22;
then p . c in {x} by A9, A63, 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 A64: ( mi < n + 1 & n <= n + 1 ) by A60, NAT_1:11, XXREAL_0:1;
then ( mi <= n & n <= ma ) by A60, NAT_1:13;
then A65: ( 1 <= n & n <= len (Co_Gen B) ) by A3, A12, XXREAL_0:2;
then n in dom (Co_Gen B) by FINSEQ_3:27;
then (Co_Gen B) . n c= (Co_Gen B) . (n + 1) by A60, A64, Th2;
then A66: ((Co_Gen B) . (n + 1)) \ ((Co_Gen B) . m1) = (((Co_Gen B) . (n + 1)) \/ ((Co_Gen B) . n)) \ ((Co_Gen B) . m1) by XBOOLE_1:12
.= ((((Co_Gen B) . (n + 1)) \ ((Co_Gen B) . n)) \/ ((Co_Gen B) . n)) \ ((Co_Gen B) . m1) by XBOOLE_1:39
.= ((((Co_Gen B) . (n + 1)) \ ((Co_Gen B) . n)) \ ((Co_Gen B) . m1)) \/ (((Co_Gen B) . n) \ ((Co_Gen B) . m1)) by XBOOLE_1:42 ;

now

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

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

then c in ((Co_Gen B) . (n + 1)) \ ((Co_Gen B) . n) by XBOOLE_0:def 5;
then A67: p . c = (FinS F,D) . (n + 1) by A1, A61, A65, Th22;

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 A10, A67, 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 A60, XXREAL_0:1;
then A68: p . c >= r by A3, A5, A10, A60, A67, RFINSEQ:32;
r >= p . c by A3, A5, A9, A60, A64, A67, RFINSEQ:32;
then r = p . c by A68, 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 ((Co_Gen B) . n) \ ((Co_Gen B) . m1) ; :: thesis: c in p " {x}

hence c in p " {x} by A59, A60, A64, A65, 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;

A69: ma in dom (Co_Gen B) by A3, A10, FINSEQ_3:31;
for n being Element of NAT holds S₂[n] from NAT_1:sch 1(A57, A58);
then cy in p " {x} by A11, A55, A69;
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 ((Co_Gen B) . ma) \ ((Co_Gen B) . m1) )
assume A70: y in p " {x} ; :: thesis: y in ((Co_Gen B) . ma) \ ((Co_Gen B) . m1)
then reconsider cy = y as Element of C ;
( cy in dom p & p . cy in {x} ) by A70, FUNCT_1:def 13;
then A71: p . cy = x by TARSKI:def 1;
assume A72: not y in ((Co_Gen B) . ma) \ ((Co_Gen B) . m1) ; :: thesis: contradiction

now

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

case A73: not y in (Co_Gen B) . ma ; :: thesis: contradiction

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

proof

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

now

assume n <= ma ; :: thesis: contradiction
then ma = len (Co_Gen B) by A3, A12, XXREAL_0:1;
then cy in (Co_Gen B) . ma by A75;
hence contradiction by A73; :: thesis: verum

end;

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

end;

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

now

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

case ma = 1m ; :: thesis: contradiction

then cy in ((Co_Gen B) . (1m + 1)) \ ((Co_Gen B) . 1m) by A73, A76, XBOOLE_0:def 5;
then p . cy = (FinS F,D) . mm by A1, A78, Th22;
hence contradiction by A10, A71, A76, A80; :: thesis: verum

end;

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

then A81: ma < 1m by A77, XXREAL_0:1;

now

assume cy in (Co_Gen B) . 1m ; :: thesis: contradiction
then mm <= 1m by A76, A79, A81;
then mm - 1m <= 0 by XREAL_1:49;
hence contradiction ; :: thesis: verum

end;

then cy in ((Co_Gen B) . (1m + 1)) \ ((Co_Gen B) . 1m) by A76, XBOOLE_0:def 5;
then p . cy = (FinS F,D) . mm by A1, A78, Th22;
hence contradiction by A10, A71, A76, A80; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

case A82: y in (Co_Gen B) . m1 ; :: thesis: contradiction

defpred S₂[ Nat] means ( $1 in dom (Co_Gen B) & $1 <= m1 & cy in (Co_Gen B) . $1 );
A83: ex n being Nat st S₂[n] by A53, A82;
consider mm being Nat such that
A84: ( S₂[mm] & ( for n being Nat st S₂[n] holds
mm <= n ) ) from NAT_1:sch 5(A83);
A85: ( 1 <= mm & mm <= len (Co_Gen B) ) by A84, 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;
A86: mm in dom (FinS F,D) by A3, A84, 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, A84, Th22;
then mi <= 1 by A9, A13, A71;
hence contradiction by A12, A51, XXREAL_0:1; :: thesis: verum

end;

case mm <> 1 ; :: thesis: contradiction

then ( 1 < mm & mm <= mm + 1 & mm < mm + 1 ) by A85, NAT_1:13, XXREAL_0:1;
then A87: ( 1 + 1 <= mm & 1m <= mm & 1m < mm ) by NAT_1:13, XREAL_1:21;
then A88: ( 1 <= 1m & 1m <= len (Co_Gen B) & 1m < len (Co_Gen B) & 1m <= m1 ) by A84, A85, XREAL_1:21, XXREAL_0:2;
then 1m in dom (Co_Gen B) by FINSEQ_3:27;
then not cy in (Co_Gen B) . 1m by A84, A87, A88;
then cy in ((Co_Gen B) . (1m + 1)) \ ((Co_Gen B) . 1m) by A84, XBOOLE_0:def 5;
then p . cy = (FinS F,D) . (1m + 1) by A1, A88, Th22;
then mi <= mm by A9, A71, A86;
then m1 + 1 <= m1 by A84, 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 A54, CARD_2:63
.= ma - (card bm1) by A3, A12, Def1
.= card ((FinS F,D) " {x}) by A3, A26, A52, 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 Rlor F,B, FinS F,D are_fiberwise_equipotent by CLASSES1:def 9; :: thesis: verum