let D be non empty set ; :: thesis: 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; :: thesis: 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 ; :: thesis: ( 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 ; :: thesis: ( 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; :: thesis: ( S2[n] implies S2[n + 1] )
assume A4: S2[n] ; :: thesis: S2[n + 1]
let Y be set ; :: thesis: 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 ; :: thesis: ( 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 ; :: thesis: 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;
now :: thesis: not x in X
assume A10: x in X ; :: thesis: contradiction
x in Y by A5, A8, A9, CARD_1:27, XBOOLE_0:def 4;
hence contradiction by A7, A10, XBOOLE_0:def 4; :: thesis: verum
end;
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}
proof
thus dom (F | (Y \ {x})) c= (dom (F | Y)) \ {x} :: according to XBOOLE_0:def 10 :: thesis: (dom (F | Y)) \ {x} c= dom (F | (Y \ {x}))
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in dom (F | (Y \ {x})) or y in (dom (F | Y)) \ {x} )
assume A14: y in dom (F | (Y \ {x})) ; :: thesis: y in (dom (F | Y)) \ {x}
then y in Y \ {x} by A12, XBOOLE_0:def 4;
then A15: not y in {x} by XBOOLE_0:def 5;
y in dom F by A12, A14, XBOOLE_0:def 4;
then y in dom (F | Y) by A12, A9, A14, XBOOLE_0:def 4;
hence y in (dom (F | Y)) \ {x} by A15, XBOOLE_0:def 5; :: thesis: verum
end;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in (dom (F | Y)) \ {x} or y in dom (F | (Y \ {x})) )
assume A16: y in (dom (F | Y)) \ {x} ; :: thesis: y in dom (F | (Y \ {x}))
then A17: not y in {x} by XBOOLE_0:def 5;
A18: y in dom (F | Y) by A16, XBOOLE_0:def 5;
then y in Y by A9, XBOOLE_0:def 4;
then A19: y in Y \ {x} by A17, XBOOLE_0:def 5;
y in dom F by A9, A18, XBOOLE_0:def 4;
hence y in dom (F | (Y \ {x})) by A12, A19, XBOOLE_0:def 4; :: thesis: verum
end;
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; :: thesis: verum
end;
A26: S2[ 0 ]
proof
let Y be set ; :: thesis: 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 ; :: thesis: ( 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 ; :: thesis: 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 ; :: thesis: verum
end;
A33: for n being Nat holds S2[n] from NAT_1:sch 2(A26, A3);
 assume X /\ Y = {} ; :: according to XBOOLE_0:def 7 :: thesis: 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; :: thesis: verum