for D being non empty set
for X being finite set
for F being PartFunc of D,REAL
for x being object st x in dom (F | X) holds
(FinS (F,(X \ {x}))) ^ <*(F . x)*>,F | X are_fiberwise_equipotent
proof
let D be non empty set ; :: thesis: for X being finite set
for F being PartFunc of D,REAL
for x being object st x in dom (F | X) holds
(FinS (F,(X \ {x}))) ^ <*(F . x)*>,F | X are_fiberwise_equipotent
let X be finite set ; :: thesis: for F being PartFunc of D,REAL
for x being object st x in dom (F | X) holds
(FinS (F,(X \ {x}))) ^ <*(F . x)*>,F | X are_fiberwise_equipotent
let F be PartFunc of D,REAL; :: thesis: for x being object st x in dom (F | X) holds
(FinS (F,(X \ {x}))) ^ <*(F . x)*>,F | X are_fiberwise_equipotent
let x be object ; :: thesis: ( x in dom (F | X) implies (FinS (F,(X \ {x}))) ^ <*(F . x)*>,F | X are_fiberwise_equipotent )
set Y = X \ {x};
set A = (FinS (F,(X \ {x}))) ^ <*(F . x)*>;
assume x in dom (F | X) ; :: thesis: (FinS (F,(X \ {x}))) ^ <*(F . x)*>,F | X are_fiberwise_equipotent
then A1: x in (dom F) /\ X by RELAT_1:61;
then x in X by XBOOLE_0:def 4;
then A2: {x} c= X by ZFMISC_1:31;
x in dom F by A1, XBOOLE_0:def 4;
then A3: {x} c= dom F by ZFMISC_1:31;
dom (F | (X \ {x})) is finite ;
then A4: F | (X \ {x}), FinS (F,(X \ {x})) are_fiberwise_equipotent by Def13;
now :: thesis: for y being object holds card (Coim ((F | X),y)) = card (Coim (((FinS (F,(X \ {x}))) ^ <*(F . x)*>),y))
let y be object ; :: thesis: card (Coim ((F | X),y)) = card (Coim (((FinS (F,(X \ {x}))) ^ <*(F . x)*>),y))
A5: X \ {x} misses {x} by XBOOLE_1:79;
A6: card (Coim ((F | (X \ {x})),y)) = card (Coim ((FinS (F,(X \ {x}))),y)) by A4, CLASSES1:def 10;
A7: dom (F | {x}) = {x} by A3, RELAT_1:62;
A8: dom <*(F . x)*> = {1} by FINSEQ_1:2, FINSEQ_1:38;
A9: now :: thesis: ( ( y = F . x & card ((F | {x}) " {y}) = card (<*(F . x)*> " {y}) ) or ( y <> F . x & card ((F | {x}) " {y}) = card (<*(F . x)*> " {y}) ) )
per cases ( y = F . x or y <> F . x ) ;
case A10: y = F . x ; :: thesis: card ((F | {x}) " {y}) = card (<*(F . x)*> " {y})
A11: {x} c= (F | {x}) " {y}
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in {x} or z in (F | {x}) " {y} )
A12: y in {y} by TARSKI:def 1;
assume A13: z in {x} ; :: thesis: z in (F | {x}) " {y}
then z = x by TARSKI:def 1;
then y = (F | {x}) . z by A7, A10, A13, FUNCT_1:47;
hence z in (F | {x}) " {y} by A7, A13, A12, FUNCT_1:def 7; :: thesis: verum
end;
(F | {x}) " {y} c= {x} by A7, RELAT_1:132;
then (F | {x}) " {y} = {x} by A11;
then A14: card ((F | {x}) " {y}) = 1 by CARD_1:30;
A15: {1} c= <*(F . x)*> " {y}
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in {1} or z in <*(F . x)*> " {y} )
A16: y in {y} by TARSKI:def 1;
assume A17: z in {1} ; :: thesis: z in <*(F . x)*> " {y}
then z = 1 by TARSKI:def 1;
then y = <*(F . x)*> . z by A10, FINSEQ_1:40;
hence z in <*(F . x)*> " {y} by A8, A17, A16, FUNCT_1:def 7; :: thesis: verum
end;
<*(F . x)*> " {y} c= {1} by A8, RELAT_1:132;
then <*(F . x)*> " {y} = {1} by A15;
hence card ((F | {x}) " {y}) = card (<*(F . x)*> " {y}) by A14, CARD_1:30; :: thesis: verum
end;
case A18: y <> F . x ; :: thesis: card ((F | {x}) " {y}) = card (<*(F . x)*> " {y})
A19: now :: thesis: not <*(F . x)*> " {y} <> {}
set z = the Element of <*(F . x)*> " {y};
assume A20: <*(F . x)*> " {y} <> {} ; :: thesis: contradiction
then <*(F . x)*> . the Element of <*(F . x)*> " {y} in {y} by FUNCT_1:def 7;
then A21: <*(F . x)*> . the Element of <*(F . x)*> " {y} = y by TARSKI:def 1;
the Element of <*(F . x)*> " {y} in {1} by A8, A20, FUNCT_1:def 7;
then the Element of <*(F . x)*> " {y} = 1 by TARSKI:def 1;
hence contradiction by A18, A21, FINSEQ_1:40; :: thesis: verum
end;
now :: thesis: not (F | {x}) " {y} <> {}
set z = the Element of (F | {x}) " {y};
assume A22: (F | {x}) " {y} <> {} ; :: thesis: contradiction
then (F | {x}) . the Element of (F | {x}) " {y} in {y} by FUNCT_1:def 7;
then A23: (F | {x}) . the Element of (F | {x}) " {y} = y by TARSKI:def 1;
A24: the Element of (F | {x}) " {y} in {x} by A7, A22, FUNCT_1:def 7;
then the Element of (F | {x}) " {y} = x by TARSKI:def 1;
hence contradiction by A7, A18, A24, A23, FUNCT_1:47; :: thesis: verum
end;
hence card ((F | {x}) " {y}) = card (<*(F . x)*> " {y}) by A19; :: thesis: verum
end;
end;
end;
A25: ((F | (X \ {x})) " {y}) \/ ((F | {x}) " {y}) = ((X \ {x}) /\ (F " {y})) \/ ((F | {x}) " {y}) by FUNCT_1:70
.= ((X \ {x}) /\ (F " {y})) \/ ({x} /\ (F " {y})) by FUNCT_1:70
.= ((X \ {x}) \/ {x}) /\ (F " {y}) by XBOOLE_1:23
.= (X \/ {x}) /\ (F " {y}) by XBOOLE_1:39
.= X /\ (F " {y}) by A2, XBOOLE_1:12
.= (F | X) " {y} by FUNCT_1:70 ;
((F | (X \ {x})) " {y}) /\ ((F | {x}) " {y}) = ((X \ {x}) /\ (F " {y})) /\ ((F | {x}) " {y}) by FUNCT_1:70
.= ((X \ {x}) /\ (F " {y})) /\ ({x} /\ (F " {y})) by FUNCT_1:70
.= (((F " {y}) /\ (X \ {x})) /\ {x}) /\ (F " {y}) by XBOOLE_1:16
.= ((F " {y}) /\ ((X \ {x}) /\ {x})) /\ (F " {y}) by XBOOLE_1:16
.= {} /\ (F " {y}) by A5
.= {} ;
hence card (Coim ((F | X),y)) = ((card ((F | (X \ {x})) " {y})) + (card (<*(F . x)*> " {y}))) - (card {}) by A25, A9, CARD_2:45
.= card (Coim (((FinS (F,(X \ {x}))) ^ <*(F . x)*>),y)) by A6, FINSEQ_3:57 ;
:: thesis: verum
end;
hence (FinS (F,(X \ {x}))) ^ <*(F . x)*>,F | X are_fiberwise_equipotent by CLASSES1:def 10; :: thesis: verum
end;
hence for D being non empty set
for d being Element of D
for X being set
for F being PartFunc of D,REAL st X is finite & d in dom (F | X) holds
(FinS (F,(X \ {d}))) ^ <*(F . d)*>,F | X are_fiberwise_equipotent ; :: thesis: verum