let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

assume A1: S_{1}[n]
; :: thesis: S_{1}[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}

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;

assume A1: S

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

assume A9:
card (dom (F | X)) = n + 1
; :: thesis: ex a being FinSequence st F | X,a are_fiberwise_equipotent
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}))

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;proof

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})) )
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;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

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

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))

hence
F | X,A are_fiberwise_equipotent
; :: thesis: verumlet 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;

.= ((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;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 ) )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
per cases
( y = F . the Element of dx or y <> F . the Element of dx )
;

end;

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}

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}

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;proof

(F | { the Element of dx}) " {y} c= { the Element of dx}
by A17, RELAT_1:132;
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;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

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

<*(F . the Element of dx)*> " {y} c= {1}
by A18, RELAT_1:132;
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;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

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

case A28:
y <> F . the Element of dx
; :: thesis: card ((F | { the Element of dx}) " {y}) = card FF

end;

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;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

now :: thesis: not (F | { the Element of dx}) " {y} <> {}

hence
card ((F | { the Element of dx}) " {y}) = card FF
by A29; :: thesis: verumset 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;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

.= ((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