let D be non empty set ; for F being PartFunc of D,REAL
for X, Y being set st dom (F | (X \/ Y)) is finite & X misses Y holds
FinS (F,(X \/ Y)),(FinS (F,X)) ^ (FinS (F,Y)) are_fiberwise_equipotent
let F be PartFunc of D,REAL; for X, Y being set st dom (F | (X \/ Y)) is finite & X misses Y holds
FinS (F,(X \/ Y)),(FinS (F,X)) ^ (FinS (F,Y)) are_fiberwise_equipotent
let X, Y be set ; ( dom (F | (X \/ Y)) is finite & X misses Y implies FinS (F,(X \/ Y)),(FinS (F,X)) ^ (FinS (F,Y)) are_fiberwise_equipotent )
assume A1:
dom (F | (X \/ Y)) is finite
; ( not X misses Y or FinS (F,(X \/ Y)),(FinS (F,X)) ^ (FinS (F,Y)) are_fiberwise_equipotent )
F | Y c= F | (X \/ Y)
by RELAT_1:75, XBOOLE_1:7;
then reconsider dfy = dom (F | Y) as finite set by A1, FINSET_1:1, RELAT_1:11;
defpred S2[ Nat] means for Y being set
for Z being finite set st Z = dom (F | Y) & dom (F | (X \/ Y)) is finite & X /\ Y = {} & $1 = card Z holds
FinS (F,(X \/ Y)),(FinS (F,X)) ^ (FinS (F,Y)) are_fiberwise_equipotent ;
A2:
card dfy = card dfy
;
A3:
for n being Nat st S2[n] holds
S2[n + 1]
proof
let n be
Nat;
( S2[n] implies S2[n + 1] )
assume A4:
S2[
n]
;
S2[n + 1]
let Y be
set ;
for Z being finite set st Z = dom (F | Y) & dom (F | (X \/ Y)) is finite & X /\ Y = {} & n + 1 = card Z holds
FinS (F,(X \/ Y)),(FinS (F,X)) ^ (FinS (F,Y)) are_fiberwise_equipotent let Z be
finite set ;
( Z = dom (F | Y) & dom (F | (X \/ Y)) is finite & X /\ Y = {} & n + 1 = card Z implies FinS (F,(X \/ Y)),(FinS (F,X)) ^ (FinS (F,Y)) are_fiberwise_equipotent )
assume that A5:
Z = dom (F | Y)
and A6:
dom (F | (X \/ Y)) is
finite
and A7:
X /\ Y = {}
and A8:
n + 1
= card Z
;
FinS (F,(X \/ Y)),(FinS (F,X)) ^ (FinS (F,Y)) are_fiberwise_equipotent
set x = the
Element of
dom (F | Y);
reconsider x = the
Element of
dom (F | Y) as
Element of
D by A5, A8, CARD_1:27, TARSKI:def 3;
set y1 =
Y \ {x};
A9:
dom (F | Y) = (dom F) /\ Y
by RELAT_1:61;
then
X \ {x} = X
by ZFMISC_1:57;
then A11:
(X \/ Y) \ {x} = X \/ (Y \ {x})
by XBOOLE_1:42;
A12:
dom (F | (Y \ {x})) = (dom F) /\ (Y \ {x})
by RELAT_1:61;
A13:
dom (F | (Y \ {x})) = (dom (F | Y)) \ {x}
then reconsider dFy =
dom (F | (Y \ {x})) as
finite set by A5;
{x} c= dom (F | Y)
by A5, A8, CARD_1:27, ZFMISC_1:31;
then A20:
card dFy =
(n + 1) - (card {x})
by A5, A8, A13, CARD_2:44
.=
(n + 1) - 1
by CARD_1:30
.=
n
;
X \/ (Y \ {x}) c= X \/ Y
by XBOOLE_1:13;
then
(dom F) /\ (X \/ (Y \ {x})) c= (dom F) /\ (X \/ Y)
by XBOOLE_1:27;
then
dom (F | (X \/ (Y \ {x}))) c= (dom F) /\ (X \/ Y)
by RELAT_1:61;
then A21:
dom (F | (X \/ (Y \ {x}))) c= dom (F | (X \/ Y))
by RELAT_1:61;
A22:
FinS (
F,
(X \/ Y)),
F | (X \/ Y) are_fiberwise_equipotent
by A6, Def13;
dom (F | (X \/ Y)) =
(dom F) /\ (X \/ Y)
by RELAT_1:61
.=
((dom F) /\ X) \/ ((dom F) /\ Y)
by XBOOLE_1:23
.=
(dom (F | X)) \/ ((dom F) /\ Y)
by RELAT_1:61
.=
(dom (F | X)) \/ (dom (F | Y))
by RELAT_1:61
;
then
x in dom (F | (X \/ Y))
by A5, A8, CARD_1:27, XBOOLE_0:def 3;
then
(FinS (F,(X \/ (Y \ {x})))) ^ <*(F . x)*>,
F | (X \/ Y) are_fiberwise_equipotent
by A6, A11, Th66;
then A23:
(FinS (F,(X \/ (Y \ {x})))) ^ <*(F . x)*>,
FinS (
F,
(X \/ Y))
are_fiberwise_equipotent
by A22, CLASSES1:76;
X /\ (Y \ {x}) c= X /\ Y
by XBOOLE_1:27;
then
FinS (
F,
(X \/ (Y \ {x}))),
(FinS (F,X)) ^ (FinS (F,(Y \ {x}))) are_fiberwise_equipotent
by A4, A6, A7, A21, A20, XBOOLE_1:3;
then
(FinS (F,(X \/ (Y \ {x})))) ^ <*(F . x)*>,
((FinS (F,X)) ^ (FinS (F,(Y \ {x})))) ^ <*(F . x)*> are_fiberwise_equipotent
by RFINSEQ:1;
then A24:
(FinS (F,(X \/ (Y \ {x})))) ^ <*(F . x)*>,
(FinS (F,X)) ^ ((FinS (F,(Y \ {x}))) ^ <*(F . x)*>) are_fiberwise_equipotent
by FINSEQ_1:32;
(
(FinS (F,(Y \ {x}))) ^ <*(F . x)*>,
F | Y are_fiberwise_equipotent &
FinS (
F,
Y),
F | Y are_fiberwise_equipotent )
by A5, A8, Def13, Th66, CARD_1:27;
then
(FinS (F,(Y \ {x}))) ^ <*(F . x)*>,
FinS (
F,
Y)
are_fiberwise_equipotent
by CLASSES1:76;
then A25:
((FinS (F,(Y \ {x}))) ^ <*(F . x)*>) ^ (FinS (F,X)),
(FinS (F,Y)) ^ (FinS (F,X)) are_fiberwise_equipotent
by RFINSEQ:1;
(FinS (F,X)) ^ ((FinS (F,(Y \ {x}))) ^ <*(F . x)*>),
((FinS (F,(Y \ {x}))) ^ <*(F . x)*>) ^ (FinS (F,X)) are_fiberwise_equipotent
by RFINSEQ:2;
then
(
(FinS (F,Y)) ^ (FinS (F,X)),
(FinS (F,X)) ^ (FinS (F,Y)) are_fiberwise_equipotent &
(FinS (F,X)) ^ ((FinS (F,(Y \ {x}))) ^ <*(F . x)*>),
(FinS (F,Y)) ^ (FinS (F,X)) are_fiberwise_equipotent )
by A25, CLASSES1:76, RFINSEQ:2;
then
(FinS (F,X)) ^ ((FinS (F,(Y \ {x}))) ^ <*(F . x)*>),
(FinS (F,X)) ^ (FinS (F,Y)) are_fiberwise_equipotent
by CLASSES1:76;
then
(FinS (F,(X \/ (Y \ {x})))) ^ <*(F . x)*>,
(FinS (F,X)) ^ (FinS (F,Y)) are_fiberwise_equipotent
by A24, CLASSES1:76;
hence
FinS (
F,
(X \/ Y)),
(FinS (F,X)) ^ (FinS (F,Y)) are_fiberwise_equipotent
by A23, CLASSES1:76;
verum
end;
A26:
S2[ 0 ]
proof
let Y be
set ;
for Z being finite set st Z = dom (F | Y) & dom (F | (X \/ Y)) is finite & X /\ Y = {} & 0 = card Z holds
FinS (F,(X \/ Y)),(FinS (F,X)) ^ (FinS (F,Y)) are_fiberwise_equipotent let Z be
finite set ;
( Z = dom (F | Y) & dom (F | (X \/ Y)) is finite & X /\ Y = {} & 0 = card Z implies FinS (F,(X \/ Y)),(FinS (F,X)) ^ (FinS (F,Y)) are_fiberwise_equipotent )
assume that A27:
Z = dom (F | Y)
and A28:
dom (F | (X \/ Y)) is
finite
and
X /\ Y = {}
and A29:
0 = card Z
;
FinS (F,(X \/ Y)),(FinS (F,X)) ^ (FinS (F,Y)) are_fiberwise_equipotent
A30:
dom (F | (X \/ Y)) =
(dom F) /\ (X \/ Y)
by RELAT_1:61
.=
((dom F) /\ X) \/ ((dom F) /\ Y)
by XBOOLE_1:23
.=
(dom (F | X)) \/ ((dom F) /\ Y)
by RELAT_1:61
.=
(dom (F | X)) \/ (dom (F | Y))
by RELAT_1:61
;
then A31:
dom (F | X) is
finite
by A28, FINSET_1:1, XBOOLE_1:7;
A32:
dom (F | Y) = {}
by A27, A29;
then FinS (
F,
(X \/ Y)) =
FinS (
F,
(dom (F | X)))
by A28, A30, Th63
.=
FinS (
F,
X)
by A31, Th63
.=
(FinS (F,X)) ^ (<*> REAL)
by FINSEQ_1:34
.=
(FinS (F,X)) ^ (FinS (F,(dom (F | Y))))
by A32, Th68
.=
(FinS (F,X)) ^ (FinS (F,Y))
by A27, Th63
;
hence
FinS (
F,
(X \/ Y)),
(FinS (F,X)) ^ (FinS (F,Y)) are_fiberwise_equipotent
;
verum
end;
A33:
for n being Nat holds S2[n]
from NAT_1:sch 2(A26, A3);
assume
X /\ Y = {}
; XBOOLE_0:def 7 FinS (F,(X \/ Y)),(FinS (F,X)) ^ (FinS (F,Y)) are_fiberwise_equipotent
hence
FinS (F,(X \/ Y)),(FinS (F,X)) ^ (FinS (F,Y)) are_fiberwise_equipotent
by A1, A33, A2; verum