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
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);
A1: ( 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;
assume A2: ( F is total & card C = card D ) ; :: thesis: Rlor (F,B), FinS (F,D) are_fiberwise_equipotent
then A3: rng (Rlor (F,B)) = rng (FinS (F,D)) by Th22;
A4: dom (Rlor (F,B)) = C by A2, Th20;
then reconsider p = Rlor (F,B) as finite PartFunc of C,REAL by FINSET_1:10;
A5: len (MIM (FinS (F,D))) = len (CHI ((Co_Gen B),C)) by A2, Th11;
A6: ( dom (FinS (F,D)) = Seg (len (FinS (F,D))) & dom (Co_Gen B) = Seg (len (Co_Gen B)) ) by FINSEQ_1:def 3;

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 A3, 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: ex n being Nat st S₁[n] by A8, FINSEQ_2:10;
consider mi being Nat such that
A10: ( S₁[mi] & ( for n being Nat st S₁[n] holds
mi <= n ) ) from NAT_1:sch 5(A9);
reconsider r = x as Real by A10;
A11: 1 <= mi by A10, 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;
A12: m1 + 1 = mi ;
A13: for n being Nat st S₁[n] holds
n <= len (FinS (F,D)) by FINSEQ_3:25;
consider ma being Nat such that
A14: ( S₁[ma] & ( for n being Nat st S₁[n] holds
n <= ma ) ) from NAT_1:sch 6(A13, A9);
A15: ma <= len (FinS (F,D)) by A14, FINSEQ_3:25;
A16: (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 A17: 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 ;
A18: y in Seg ma by A17, XBOOLE_0:def 5;
then A19: 1 <= l by FINSEQ_1:1;
A20: l <= ma by A18, FINSEQ_1:1;
then l <= len (FinS (F,D)) by A15, XXREAL_0:2;
then A21: l in dom (FinS (F,D)) by A19, FINSEQ_3:25;
not y in Seg m1 by A17, XBOOLE_0:def 5;
then ( l < 1 or m1 < l ) by FINSEQ_1:1;
then mi < l + 1 by A18, FINSEQ_1:1, XREAL_1:19;
then A22: 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 A14, TARSKI:def 1;
hence y in (FinS (F,D)) " {x} by A21, FUNCT_1:def 7; :: thesis: verum

end;

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

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

end;

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

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

end;

A29: 1 <= ma by A14, FINSEQ_3:25;
A30: mi <= ma by A10, A14;
m1 <= mi by XREAL_1:43;
then A31: m1 <= ma by A30, XXREAL_0:2;
then Seg m1 c= Seg ma by FINSEQ_1:5;
then A32: card ((FinS (F,D)) " {x}) = (card (Seg ma)) - (card (Seg m1)) by A16, CARD_2:44
.= ma - (card (Seg m1)) by FINSEQ_1:57
.= ma - m1 by FINSEQ_1:57 ;
A33: mi <= len (FinS (F,D)) by A10, FINSEQ_3:25;
then 1 <= len (FinS (F,D)) by A11, XXREAL_0:2;
then A34: 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 A35: 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

defpred S₂[ 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} );
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in (Co_Gen B) . ma or y in p " {x} )
assume A36: y in (Co_Gen B) . ma ; :: thesis: y in p " {x}
(Co_Gen B) . ma c= C by A5, A1, A6, A14, Lm5;
then reconsider cy = y as Element of C by A36;
A37: for n being Nat st S₂[n] holds
S₂[n + 1]

proof

let n be Nat; :: thesis: ( S₂[n] implies S₂[n + 1] )
assume A38: S₂[n] ; :: thesis: S₂[n + 1]
assume that
A39: n + 1 in dom (Co_Gen B) and
A40: n + 1 <= ma ; :: thesis: for c being Element of C st c in (Co_Gen B) . (n + 1) holds
c in p " {x}
A41: n + 1 <= len (Co_Gen B) by A39, FINSEQ_3:25;
then A42: n <= (len (Co_Gen B)) - 1 by XREAL_1:19;
A43: n < len (Co_Gen B) by A41, NAT_1:13;
let c be Element of C; :: thesis: ( c in (Co_Gen B) . (n + 1) implies c in p " {x} )
assume A44: c in (Co_Gen B) . (n + 1) ; :: thesis: c in p " {x}
A45: n <= len (Co_Gen B) by A41, 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 A2, A10, A35, A44, Th21;
then p . c in {x} by TARSKI:def 1;
hence c in p " {x} by A4, FUNCT_1:def 7; :: thesis: verum

end;

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

then A47: 0 + 1 < n + 1 by XREAL_1:6;
A48: 0 + 1 <= n by A46, NAT_1:13;
then (Co_Gen B) . n c= (Co_Gen B) . (n + 1) by A42, Def2;
then A49: (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 :: thesis: ( ( c in ((Co_Gen B) . (n + 1)) \ ((Co_Gen B) . n) & c in p " {x} ) or ( c in (Co_Gen B) . n & c in p " {x} ) )

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

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

then A50: p . c = (FinS (F,D)) . (n + 1) by A2, A43, A48, Th21;

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

end;

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

then n + 1 < ma by A40, XXREAL_0:1;
then A51: p . c >= r by A5, A1, A6, A14, A39, A50, RFINSEQ:19;
r >= p . c by A5, A1, A6, A10, A35, A39, A47, A50, RFINSEQ:19;
then r = p . c by A51, XXREAL_0:1;
then p . c in {x} by TARSKI:def 1;
hence c in p " {x} by A4, FUNCT_1:def 7; :: 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 A38, A40, A45, A48, 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;

A52: S₂[ 0 ] by FINSEQ_3:25;
A53: for n being Nat holds S₂[n] from NAT_1:sch 2(A52, A37);
ma in dom (Co_Gen B) by A5, A1, A14, FINSEQ_3:29;
then cy in p " {x} by A36, A53;
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 (Co_Gen B) . ma )
assume A54: y in p " {x} ; :: thesis: y in (Co_Gen B) . ma
then reconsider cy = y as Element of C ;
p . cy in {x} by A54, FUNCT_1:def 7;
then A55: 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 );
assume A56: not y in (Co_Gen B) . ma ; :: thesis: contradiction
A57: ex n being Nat st S₂[n]

proof

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

now :: thesis: not n <= ma

assume n <= ma ; :: thesis: contradiction
then ma = len (Co_Gen B) by A5, A1, A15, XXREAL_0:1;
then cy in (Co_Gen B) . ma by A58;
hence contradiction by A56; :: thesis: verum

end;

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

end;

consider mm being Nat such that
A59: ( S₂[mm] & ( for n being Nat st S₂[n] holds
mm <= n ) ) from NAT_1:sch 5(A57);
1 <= mm by A59, 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 A59, NAT_1:13;
then A60: ma <= 1m by XREAL_1:19;
then A61: 1 <= 1m by A29, XXREAL_0:2;
A62: mm in dom (FinS (F,D)) by A5, A1, A59, FINSEQ_3:29;
A63: mm <= len (Co_Gen B) by A59, FINSEQ_3:25;
A64: mm < mm + 1 by NAT_1:13;
then 1m < mm by XREAL_1:19;
then A65: 1m < len (Co_Gen B) by A63, XXREAL_0:2;
1m <= mm by A64, XREAL_1:19;
then 1m <= len (Co_Gen B) by A63, XXREAL_0:2;
then A66: 1m in dom (Co_Gen B) by A61, 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 ((Co_Gen B) . (1m + 1)) \ ((Co_Gen B) . 1m) by A56, A59, XBOOLE_0:def 5;
then p . cy = (FinS (F,D)) . mm by A2, A61, A65, Th21;
hence contradiction by A14, A55, A59, A62; :: thesis: verum

end;

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

then A67: ma < 1m by A60, XXREAL_0:1;

now :: thesis: not cy in (Co_Gen B) . 1m

assume cy in (Co_Gen B) . 1m ; :: thesis: contradiction
then mm <= 1m by A59, A66, A67;
then mm - 1m <= 0 by XREAL_1:47;
hence contradiction ; :: thesis: verum

end;

then cy in ((Co_Gen B) . (1m + 1)) \ ((Co_Gen B) . 1m) by A59, XBOOLE_0:def 5;
then p . cy = (FinS (F,D)) . mm by A2, A61, A65, Th21;
hence contradiction by A14, A55, A59, A62; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

hence card (p " {x}) = card ((FinS (F,D)) " {x}) by A5, A1, A29, A15, A32, A35, Def1; :: thesis: verum

end;

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

then 1 < mi by A11, XXREAL_0:1;
then A69: 1 <= m1 by A12, NAT_1:13;
A70: m1 <= len (FinS (F,D)) by A33, A12, NAT_1:13;
then A71: m1 in dom (Co_Gen B) by A5, A1, A69, FINSEQ_3:25;
then A72: (Co_Gen B) . m1 c= (Co_Gen B) . ma by A5, A1, A6, A14, A31, Th2;
(Co_Gen B) . ma c= C by A5, A1, A6, A14, Lm5;
then reconsider bma = (Co_Gen B) . ma, bm1 = (Co_Gen B) . m1 as finite set by A72;
((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

defpred S₂[ 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} );
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in ((Co_Gen B) . ma) \ ((Co_Gen B) . m1) or y in p " {x} )
A73: (Co_Gen B) . ma c= C by A5, A1, A6, A14, Lm5;
A74: for n being Nat st S₂[n] holds
S₂[n + 1]

proof

let n be Nat; :: thesis: ( S₂[n] implies S₂[n + 1] )
assume A75: S₂[n] ; :: thesis: S₂[n + 1]
assume that
A76: n + 1 in dom (Co_Gen B) and
A77: mi <= n + 1 and
A78: 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}
let c be Element of C; :: thesis: ( c in ((Co_Gen B) . (n + 1)) \ ((Co_Gen B) . m1) implies c in p " {x} )
n + 1 <= len (Co_Gen B) by A76, FINSEQ_3:25;
then A79: n < len (Co_Gen B) by NAT_1:13;
assume A80: c in ((Co_Gen B) . (n + 1)) \ ((Co_Gen 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 A81: n + 1 = mi ; :: thesis: c in p " {x}

then p . c = (FinS (F,D)) . (n + 1) by A2, A69, A79, A80, Th21;
then p . c in {x} by A10, A81, TARSKI:def 1;
hence c in p " {x} by A4, FUNCT_1:def 7; :: thesis: verum

end;

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

then A82: mi < n + 1 by A77, XXREAL_0:1;
then mi <= n by NAT_1:13;
then A83: 1 <= n by A11, XXREAL_0:2;
n <= ma by A78, NAT_1:13;
then A84: n <= len (Co_Gen B) by A5, A1, A15, XXREAL_0:2;
then ( n <= n + 1 & n in dom (Co_Gen B) ) by A83, FINSEQ_3:25, NAT_1:11;
then (Co_Gen B) . n c= (Co_Gen B) . (n + 1) by A76, Th2;
then A85: ((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 :: thesis: ( ( c in (((Co_Gen B) . (n + 1)) \ ((Co_Gen B) . n)) \ ((Co_Gen B) . m1) & c in p " {x} ) or ( c in ((Co_Gen B) . n) \ ((Co_Gen B) . m1) & c in p " {x} ) )

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 A80, A85, 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 A86: p . c = (FinS (F,D)) . (n + 1) by A2, A79, A83, Th21;

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

end;

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

then n + 1 < ma by A78, XXREAL_0:1;
then A87: p . c >= r by A5, A1, A6, A14, A76, A86, RFINSEQ:19;
r >= p . c by A5, A1, A6, A10, A76, A82, A86, RFINSEQ:19;
then r = p . c by A87, XXREAL_0:1;
then p . c in {x} by TARSKI:def 1;
hence c in p " {x} by A4, FUNCT_1:def 7; :: 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 A75, A78, A82, A83, A84, 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;

A88: S₂[ 0 ] ;
A89: for n being Nat holds S₂[n] from NAT_1:sch 2(A88, A74);
assume A90: y in ((Co_Gen B) . ma) \ ((Co_Gen B) . m1) ; :: thesis: y in p " {x}
then y in (Co_Gen B) . ma ;
then reconsider cy = y as Element of C by A73;
ma in dom (Co_Gen B) by A5, A1, A14, FINSEQ_3:29;
then cy in p " {x} by A30, A90, A89;
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 ((Co_Gen B) . ma) \ ((Co_Gen B) . m1) )
assume A91: y in p " {x} ; :: thesis: y in ((Co_Gen B) . ma) \ ((Co_Gen B) . m1)
then reconsider cy = y as Element of C ;
p . cy in {x} by A91, FUNCT_1:def 7;
then A92: p . cy = x by TARSKI:def 1;
assume A93: not y in ((Co_Gen B) . ma) \ ((Co_Gen B) . m1) ; :: thesis: contradiction

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

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

case A94: 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 );
A95: ex n being Nat st S₂[n]

proof

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

now :: thesis: not n <= ma

assume n <= ma ; :: thesis: contradiction
then ma = len (Co_Gen B) by A5, A1, A15, XXREAL_0:1;
then cy in (Co_Gen B) . ma by A96;
hence contradiction by A94; :: thesis: verum

end;

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

end;

consider mm being Nat such that
A97: ( S₂[mm] & ( for n being Nat st S₂[n] holds
mm <= n ) ) from NAT_1:sch 5(A95);
1 <= mm by A97, 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 A97, NAT_1:13;
then A98: ma <= 1m by XREAL_1:19;
then A99: 1 <= 1m by A29, XXREAL_0:2;
A100: mm in dom (FinS (F,D)) by A5, A1, A97, FINSEQ_3:29;
A101: mm <= len (Co_Gen B) by A97, FINSEQ_3:25;
A102: mm < mm + 1 by NAT_1:13;
then 1m < mm by XREAL_1:19;
then A103: 1m < len (Co_Gen B) by A101, XXREAL_0:2;
1m <= mm by A102, XREAL_1:19;
then 1m <= len (Co_Gen B) by A101, XXREAL_0:2;
then A104: 1m in dom (Co_Gen B) by A99, 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 ((Co_Gen B) . (1m + 1)) \ ((Co_Gen B) . 1m) by A94, A97, XBOOLE_0:def 5;
then p . cy = (FinS (F,D)) . mm by A2, A99, A103, Th21;
hence contradiction by A14, A92, A97, A100; :: thesis: verum

end;

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

then A105: ma < 1m by A98, XXREAL_0:1;

now :: thesis: not cy in (Co_Gen B) . 1m

assume cy in (Co_Gen B) . 1m ; :: thesis: contradiction
then mm <= 1m by A97, A104, A105;
then mm - 1m <= 0 by XREAL_1:47;
hence contradiction ; :: thesis: verum

end;

then cy in ((Co_Gen B) . (1m + 1)) \ ((Co_Gen B) . 1m) by A97, XBOOLE_0:def 5;
then p . cy = (FinS (F,D)) . mm by A2, A99, A103, Th21;
hence contradiction by A14, A92, A97, A100; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

case A106: 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 );
A107: ex n being Nat st S₂[n] by A71, A106;
consider mm being Nat such that
A108: ( S₂[mm] & ( for n being Nat st S₂[n] holds
mm <= n ) ) from NAT_1:sch 5(A107);
A109: 1 <= mm by A108, 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;
A110: mm <= len (Co_Gen B) by A108, FINSEQ_3:25;
A111: mm in dom (FinS (F,D)) by A5, A1, A108, 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 A2, A108, Th21;
then mi <= 1 by A10, A34, A92;
hence contradiction by A11, A68, XXREAL_0:1; :: thesis: verum

end;

case mm <> 1 ; :: thesis: contradiction

then 1 < mm by A109, XXREAL_0:1;
then 1 + 1 <= mm by NAT_1:13;
then A112: 1 <= 1m by XREAL_1:19;
A113: mm < mm + 1 by NAT_1:13;
then A114: 1m <= mm by XREAL_1:19;
then 1m <= len (Co_Gen B) by A110, XXREAL_0:2;
then A115: 1m in dom (Co_Gen B) by A112, FINSEQ_3:25;
A116: 1m < mm by A113, XREAL_1:19;
then A117: 1m < len (Co_Gen B) by A110, XXREAL_0:2;
1m <= m1 by A108, A114, XXREAL_0:2;
then not cy in (Co_Gen B) . 1m by A108, A116, A115;
then cy in ((Co_Gen B) . (1m + 1)) \ ((Co_Gen B) . 1m) by A108, XBOOLE_0:def 5;
then p . cy = (FinS (F,D)) . (1m + 1) by A2, A112, A117, Th21;
then mi <= mm by A10, A92, A111;
then m1 + 1 <= m1 by A108, 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 A72, CARD_2:44
.= ma - (card bm1) by A5, A1, A29, A15, Def1
.= card ((FinS (F,D)) " {x}) by A5, A1, A32, A69, A70, 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 10; :: thesis: verum