let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume A1: S1[n] ; :: thesis: S1[n + 1]
let X be finite set ; :: thesis: for F being Function st card (dom (F | X)) = n + 1 holds
ex a being FinSequence st F | X,a are_fiberwise_equipotent
let F be Function; :: thesis: ( card (dom (F | X)) = n + 1 implies ex a being FinSequence st F | X,a are_fiberwise_equipotent )
reconsider dx = dom (F | X) as finite set ;
set x = the Element of dx;
set Y = X \ { the Element of dx};
set dy = dom (F | (X \ { the Element of dx}));
A2: dom (F | (X \ { the Element of dx})) = (dom F) /\ (X \ { the Element of dx}) by RELAT_1:61;
A3: dx = (dom F) /\ X by RELAT_1:61;
A4: dom (F | (X \ { the Element of dx})) = dx \ { the Element of dx}
proof
thus dom (F | (X \ { the Element of dx})) c= dx \ { the Element of dx} :: according to XBOOLE_0:def 10 :: thesis: dx \ { the Element of dx} c= dom (F | (X \ { the Element of dx}))
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in dom (F | (X \ { the Element of dx})) or y in dx \ { the Element of dx} )
assume A5: y in dom (F | (X \ { the Element of dx})) ; :: thesis: y in dx \ { the Element of dx}
then y in X \ { the Element of dx} by A2, XBOOLE_0:def 4;
then A6: not y in { the Element of dx} by XBOOLE_0:def 5;
y in dom F by A2, A5, XBOOLE_0:def 4;
then y in dx by A2, A3, A5, XBOOLE_0:def 4;
hence y in dx \ { the Element of dx} by A6, XBOOLE_0:def 5; :: thesis: verum
end;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in dx \ { the Element of dx} or y in dom (F | (X \ { the Element of dx})) )
assume A7: y in dx \ { the Element of dx} ; :: thesis: y in dom (F | (X \ { the Element of dx}))
then ( not y in { the Element of dx} & y in X ) by A3, XBOOLE_0:def 4, XBOOLE_0:def 5;
then A8: y in X \ { the Element of dx} by XBOOLE_0:def 5;
y in dom F by A3, A7, XBOOLE_0:def 4;
hence y in dom (F | (X \ { the Element of dx})) by A2, A8, XBOOLE_0:def 4; :: thesis: verum
end;
assume A9: card (dom (F | X)) = n + 1 ; :: thesis: ex a being FinSequence st F | X,a are_fiberwise_equipotent
then { the Element of dx} c= dx by CARD_1:27, ZFMISC_1:31;
then card (dom (F | (X \ { the Element of dx}))) = (card dx) - (card { the Element of dx}) by A4, CARD_2:44
.= (n + 1) - 1 by A9, CARD_1:30
.= n ;
then consider a being FinSequence such that
A10: F | (X \ { the Element of dx}),a are_fiberwise_equipotent by A1;
take A = a ^ <*(F . the Element of dx)*>; :: thesis: F | X,A are_fiberwise_equipotent
dx <> {} by A9;
then the Element of dx in dx ;
then A11: the Element of dx in (dom F) /\ X by RELAT_1:61;
then the Element of dx in dom F by XBOOLE_0:def 4;
then A12: { the Element of dx} c= dom F by ZFMISC_1:31;
the Element of dx in X by A11, XBOOLE_0:def 4;
then A13: { the Element of dx} c= X by ZFMISC_1:31;
now :: thesis: for y being object holds card (Coim ((F | X),y)) = card (Coim (A,y))
let y be object ; :: thesis: card (Coim ((F | X),y)) = card (Coim (A,y))
A14: X \ { the Element of dx} misses { the Element of dx} by XBOOLE_1:79;
A15: ((F | (X \ { the Element of dx})) " {y}) \/ ((F | { the Element of dx}) " {y}) = ((X \ { the Element of dx}) /\ (F " {y})) \/ ((F | { the Element of dx}) " {y}) by FUNCT_1:70
.= ((X \ { the Element of dx}) /\ (F " {y})) \/ ({ the Element of dx} /\ (F " {y})) by FUNCT_1:70
.= ((X \ { the Element of dx}) \/ { the Element of dx}) /\ (F " {y}) by XBOOLE_1:23
.= (X \/ { the Element of dx}) /\ (F " {y}) by XBOOLE_1:39
.= X /\ (F " {y}) by A13, XBOOLE_1:12
.= (F | X) " {y} by FUNCT_1:70 ;
reconsider FF = <*(F . the Element of dx)*> " {y} as finite set ;
A16: card (Coim ((F | (X \ { the Element of dx})),y)) = card (Coim (a,y)) by A10;
A17: dom (F | { the Element of dx}) = { the Element of dx} by A12, RELAT_1:62;
A18: dom <*(F . the Element of dx)*> = {1} by FINSEQ_1:2, FINSEQ_1:38;
A19: now :: thesis: ( ( y = F . the Element of dx & card ((F | { the Element of dx}) " {y}) = card FF ) or ( y <> F . the Element of dx & card ((F | { the Element of dx}) " {y}) = card FF ) )
per cases ( y = F . the Element of dx or y <> F . the Element of dx ) ;
case A20: y = F . the Element of dx ; :: thesis: card ((F | { the Element of dx}) " {y}) = card FF
A21: { the Element of dx} c= (F | { the Element of dx}) " {y}
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in { the Element of dx} or z in (F | { the Element of dx}) " {y} )
A22: y in {y} by TARSKI:def 1;
assume A23: z in { the Element of dx} ; :: thesis: z in (F | { the Element of dx}) " {y}
then z = the Element of dx by TARSKI:def 1;
then y = (F | { the Element of dx}) . z by A17, A20, A23, FUNCT_1:47;
hence z in (F | { the Element of dx}) " {y} by A17, A23, A22, FUNCT_1:def 7; :: thesis: verum
end;
(F | { the Element of dx}) " {y} c= { the Element of dx} by A17, RELAT_1:132;
then (F | { the Element of dx}) " {y} = { the Element of dx} by A21;
then A24: card ((F | { the Element of dx}) " {y}) = 1 by CARD_1:30;
A25: {1} c= <*(F . the Element of dx)*> " {y}
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in {1} or z in <*(F . the Element of dx)*> " {y} )
A26: y in {y} by TARSKI:def 1;
assume A27: z in {1} ; :: thesis: z in <*(F . the Element of dx)*> " {y}
then z = 1 by TARSKI:def 1;
then y = <*(F . the Element of dx)*> . z by A20, FINSEQ_1:40;
hence z in <*(F . the Element of dx)*> " {y} by A18, A27, A26, FUNCT_1:def 7; :: thesis: verum
end;
<*(F . the Element of dx)*> " {y} c= {1} by A18, RELAT_1:132;
then <*(F . the Element of dx)*> " {y} = {1} by A25;
hence card ((F | { the Element of dx}) " {y}) = card FF by A24, CARD_1:30; :: thesis: verum
end;
case A28: y <> F . the Element of dx ; :: thesis: card ((F | { the Element of dx}) " {y}) = card FF
A29: now :: thesis: not <*(F . the Element of dx)*> " {y} <> {}
set z = the Element of <*(F . the Element of dx)*> " {y};
assume A30: <*(F . the Element of dx)*> " {y} <> {} ; :: thesis: contradiction
then <*(F . the Element of dx)*> . the Element of <*(F . the Element of dx)*> " {y} in {y} by FUNCT_1:def 7;
then A31: <*(F . the Element of dx)*> . the Element of <*(F . the Element of dx)*> " {y} = y by TARSKI:def 1;
the Element of <*(F . the Element of dx)*> " {y} in {1} by A18, A30, FUNCT_1:def 7;
then the Element of <*(F . the Element of dx)*> " {y} = 1 by TARSKI:def 1;
hence contradiction by A28, A31, FINSEQ_1:40; :: thesis: verum
end;
now :: thesis: not (F | { the Element of dx}) " {y} <> {}
set z = the Element of (F | { the Element of dx}) " {y};
assume A32: (F | { the Element of dx}) " {y} <> {} ; :: thesis: contradiction
then (F | { the Element of dx}) . the Element of (F | { the Element of dx}) " {y} in {y} by FUNCT_1:def 7;
then A33: (F | { the Element of dx}) . the Element of (F | { the Element of dx}) " {y} = y by TARSKI:def 1;
A34: the Element of (F | { the Element of dx}) " {y} in { the Element of dx} by A17, A32, FUNCT_1:def 7;
then the Element of (F | { the Element of dx}) " {y} = the Element of dx by TARSKI:def 1;
hence contradiction by A17, A28, A34, A33, FUNCT_1:47; :: thesis: verum
end;
hence card ((F | { the Element of dx}) " {y}) = card FF by A29; :: thesis: verum
end;
end;
end;
((F | (X \ { the Element of dx})) " {y}) /\ ((F | { the Element of dx}) " {y}) = ((X \ { the Element of dx}) /\ (F " {y})) /\ ((F | { the Element of dx}) " {y}) by FUNCT_1:70
.= ((X \ { the Element of dx}) /\ (F " {y})) /\ ({ the Element of dx} /\ (F " {y})) by FUNCT_1:70
.= (((F " {y}) /\ (X \ { the Element of dx})) /\ { the Element of dx}) /\ (F " {y}) by XBOOLE_1:16
.= ((F " {y}) /\ ((X \ { the Element of dx}) /\ { the Element of dx})) /\ (F " {y}) by XBOOLE_1:16
.= {} /\ (F " {y}) by A14
.= {} ;
hence card (Coim ((F | X),y)) = ((card ((F | (X \ { the Element of dx})) " {y})) + (card FF)) - (card {}) by A15, A19, CARD_2:45
.= card (Coim (A,y)) by A16, FINSEQ_3:57 ;
:: thesis: verum
end;
hence F | X,A are_fiberwise_equipotent ; :: thesis: verum