let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A1: S₁[n] ; :: thesis: S₁[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 ;
consider x being Element of dx;
set Y = X \ {x};
set dy = dom (F | (X \ {x}));
A2: dom (F | (X \ {x})) = (dom F) /\ (X \ {x}) by RELAT_1:90;
A3: dx = (dom F) /\ X by RELAT_1:90;
A4: dom (F | (X \ {x})) = dx \ {x}

proof

thus dom (F | (X \ {x})) c= dx \ {x} :: according to XBOOLE_0:def 10 :: thesis: dx \ {x} c= dom (F | (X \ {x}))

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in dom (F | (X \ {x})) or y in dx \ {x} )
assume A5: y in dom (F | (X \ {x})) ; :: thesis: y in dx \ {x}
then y in X \ {x} by A2, XBOOLE_0:def 4;
then A6: not y in {x} 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 \ {x} by A6, XBOOLE_0:def 5; :: thesis: verum

end;

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in dx \ {x} or y in dom (F | (X \ {x})) )
assume A7: y in dx \ {x} ; :: thesis: y in dom (F | (X \ {x}))
then ( not y in {x} & y in X ) by A3, XBOOLE_0:def 4, XBOOLE_0:def 5;
then A8: y in X \ {x} by XBOOLE_0:def 5;
y in dom F by A3, A7, XBOOLE_0:def 4;
hence y in dom (F | (X \ {x})) 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 {x} c= dx by CARD_1:47, ZFMISC_1:37;
then card (dom (F | (X \ {x}))) = (card dx) - (card {x}) by A4, CARD_2:63
.= (n + 1) - 1 by A9, CARD_1:50
.= n ;
then consider a being FinSequence such that
A10: F | (X \ {x}),a are_fiberwise_equipotent by A1;
take A = a ^ <*(F . x)*>; :: thesis: F | X,A are_fiberwise_equipotent
dx <> {} by A9;
then x in dx ;
then A11: x in (dom F) /\ X by RELAT_1:90;
then x in dom F by XBOOLE_0:def 4;
then A12: {x} c= dom F by ZFMISC_1:37;
x in X by A11, XBOOLE_0:def 4;
then A13: {x} c= X by ZFMISC_1:37;

now

let y be set ; :: thesis: card (Coim (F | X),y) = card (Coim A,y)
A14: X \ {x} misses {x} by XBOOLE_1:79;
A15: ((F | (X \ {x})) " {y}) \/ ((F | {x}) " {y}) = ((X \ {x}) /\ (F " {y})) \/ ((F | {x}) " {y}) by FUNCT_1:139
.= ((X \ {x}) /\ (F " {y})) \/ ({x} /\ (F " {y})) by FUNCT_1:139
.= ((X \ {x}) \/ {x}) /\ (F " {y}) by XBOOLE_1:23
.= (X \/ {x}) /\ (F " {y}) by XBOOLE_1:39
.= X /\ (F " {y}) by A13, XBOOLE_1:12
.= (F | X) " {y} by FUNCT_1:139 ;
reconsider FF = <*(F . x)*> " {y} as finite set ;
A16: card (Coim (F | (X \ {x})),y) = card (Coim a,y) by A10, CLASSES1:def 9;
A17: dom (F | {x}) = {x} by A12, RELAT_1:91;
A18: dom <*(F . x)*> = {1} by FINSEQ_1:4, FINSEQ_1:55;

A19: now

per cases ( y = F . x or y <> F . x ) ;

case A20: y = F . x ; :: thesis: card ((F | {x}) " {y}) = card FF

A21: {x} c= (F | {x}) " {y}

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in {x} or z in (F | {x}) " {y} )
A22: y in {y} by TARSKI:def 1;
assume A23: z in {x} ; :: thesis: z in (F | {x}) " {y}
then z = x by TARSKI:def 1;
then y = (F | {x}) . z by A17, A20, A23, FUNCT_1:70;
hence z in (F | {x}) " {y} by A17, A23, A22, FUNCT_1:def 13; :: thesis: verum

end;

(F | {x}) " {y} c= {x} by A17, RELAT_1:167;
then (F | {x}) " {y} = {x} by A21, XBOOLE_0:def 10;
then A24: card ((F | {x}) " {y}) = 1 by CARD_1:50;
A25: {1} c= <*(F . x)*> " {y}

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in {1} or z in <*(F . x)*> " {y} )
A26: y in {y} by TARSKI:def 1;
assume A27: z in {1} ; :: thesis: z in <*(F . x)*> " {y}
then z = 1 by TARSKI:def 1;
then y = <*(F . x)*> . z by A20, FINSEQ_1:57;
hence z in <*(F . x)*> " {y} by A18, A27, A26, FUNCT_1:def 13; :: thesis: verum

end;

<*(F . x)*> " {y} c= {1} by A18, RELAT_1:167;
then <*(F . x)*> " {y} = {1} by A25, XBOOLE_0:def 10;
hence card ((F | {x}) " {y}) = card FF by A24, CARD_1:50; :: thesis: verum

end;

case A28: y <> F . x ; :: thesis: card ((F | {x}) " {y}) = card FF

A29: now

consider z being Element of <*(F . x)*> " {y};
assume A30: <*(F . x)*> " {y} <> {} ; :: thesis: contradiction
then <*(F . x)*> . z in {y} by FUNCT_1:def 13;
then A31: <*(F . x)*> . z = y by TARSKI:def 1;
z in {1} by A18, A30, FUNCT_1:def 13;
then z = 1 by TARSKI:def 1;
hence contradiction by A28, A31, FINSEQ_1:57; :: thesis: verum

end;

now

consider z being Element of (F | {x}) " {y};
assume A32: (F | {x}) " {y} <> {} ; :: thesis: contradiction
then (F | {x}) . z in {y} by FUNCT_1:def 13;
then A33: (F | {x}) . z = y by TARSKI:def 1;
A34: z in {x} by A17, A32, FUNCT_1:def 13;
then z = x by TARSKI:def 1;
hence contradiction by A17, A28, A34, A33, FUNCT_1:70; :: thesis: verum

end;

hence card ((F | {x}) " {y}) = card FF by A29; :: thesis: verum

end;

end;

end;

((F | (X \ {x})) " {y}) /\ ((F | {x}) " {y}) = ((X \ {x}) /\ (F " {y})) /\ ((F | {x}) " {y}) by FUNCT_1:139
.= ((X \ {x}) /\ (F " {y})) /\ ({x} /\ (F " {y})) by FUNCT_1:139
.= (((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 A14, XBOOLE_0:def 7
.= {} ;
hence card (Coim (F | X),y) = ((card ((F | (X \ {x})) " {y})) + (card FF)) - (card {} ) by A15, A19, CARD_2:64
.= card (Coim A,y) by A16, FINSEQ_3:63 ;
:: thesis: verum

end;

hence F | X,A are_fiberwise_equipotent by CLASSES1:def 9; :: thesis: verum