let X be set ; :: thesis: for Y being non empty finite set st card X = (card Y) + 1 holds
for f being Function of X,Y st f is onto holds
ex y being set st
( y in Y & card (f " {y}) = 2 & ( for x being set st x in Y & x <> y holds
card (f " {x}) = 1 ) )
let Y be non empty finite set ; :: thesis: ( card X = (card Y) + 1 implies for f being Function of X,Y st f is onto holds
ex y being set st
( y in Y & card (f " {y}) = 2 & ( for x being set st x in Y & x <> y holds
card (f " {x}) = 1 ) ) )
assume A1: card X = (card Y) + 1 ; :: thesis: for f being Function of X,Y st f is onto holds
ex y being set st
( y in Y & card (f " {y}) = 2 & ( for x being set st x in Y & x <> y holds
card (f " {x}) = 1 ) )
reconsider XX = X as non empty finite set by A1;
card Y > 0 ;
then reconsider c1 = (card Y) - 1 as Element of NAT by NAT_1:20;
let f be Function of X,Y; :: thesis: ( f is onto implies ex y being set st
( y in Y & card (f " {y}) = 2 & ( for x being set st x in Y & x <> y holds
card (f " {x}) = 1 ) ) )
assume A2: f is onto ; :: thesis: ex y being set st
( y in Y & card (f " {y}) = 2 & ( for x being set st x in Y & x <> y holds
card (f " {x}) = 1 ) )
A3: rng f = Y by A2, FUNCT_2:def 3;
reconsider F = f as Function of XX,Y ;
A4: dom f = X by FUNCT_2:def 1;
ex y being set st
( y in Y & card (F " {y}) > 1 )

proof

assume A5: for y being set st y in Y holds
card (F " {y}) <= 1 ; :: thesis: contradiction

now :: thesis: for y being object st y in Y holds
ex x being object st F " {y} = {x}

let y be object ; :: thesis: ( y in Y implies ex x being object st F " {y} = {x} )
set fy = F " {y};
assume A6: y in Y ; :: thesis: ex x being object st F " {y} = {x}
then F " {y} <> {} by A3, FUNCT_1:72;
then card (F " {y}) = 1 by A5, A6, NAT_1:25;
hence ex x being object st F " {y} = {x} by CARD_2:42; :: thesis: verum

end;

then f is one-to-one by A3, FUNCT_1:74;
then X,Y are_equipotent by A3, A4, WELLORD2:def 4;
then card X = card Y by CARD_1:5;
hence contradiction by A1; :: thesis: verum

end;

then consider y being set such that
A7: y in Y and
A8: card (F " {y}) > 1 ;
set fy = F " {y};
set fD = F | ((dom f) \ (F " {y}));
take y ; :: thesis: ( y in Y & card (f " {y}) = 2 & ( for x being set st x in Y & x <> y holds
card (f " {x}) = 1 ) )
A9: 1 + 1 <= card (F " {y}) by A8, NAT_1:13;
dom (F | ((dom f) \ (F " {y}))) = (dom f) \ (F " {y}) by RELAT_1:62, XBOOLE_1:36;
then A10: card (dom (F | ((dom f) \ (F " {y})))) = (card XX) - (card (F " {y})) by A4, CARD_2:44;
set Yy = Y \ {y};
A11: rng (F | ((dom f) \ (F " {y}))) = Y \ {y} by A3, STIRL2_1:54;
then reconsider FD = F | ((dom f) \ (F " {y})) as Function of (dom (F | ((dom f) \ (F " {y})))),(Y \ {y}) by FUNCT_2:1;
card Y = c1 + 1 ;
then A12: card (Y \ {y}) = c1 by A7, STIRL2_1:55;
then Segm c1 c= Segm (card (dom (F | ((dom f) \ (F " {y}))))) by A11, CARD_1:12;
then (card Y) + (- 1) <= (card Y) + (1 - (card (F " {y}))) by A1, A10, NAT_1:39;
then - 1 <= 1 - (card (F " {y})) by XREAL_1:6;
then card (F " {y}) <= 1 - (- 1) by XREAL_1:11;
hence A13: ( y in Y & card (f " {y}) = 2 ) by A7, A9, XXREAL_0:1; :: thesis: for x being set st x in Y & x <> y holds
card (f " {x}) = 1
let x be set ; :: thesis: ( x in Y & x <> y implies card (f " {x}) = 1 )
assume that
A14: x in Y and
A15: x <> y ; :: thesis: card (f " {x}) = 1
A16: x in rng FD by A11, A14, A15, ZFMISC_1:56;
FD is onto by A11, FUNCT_2:def 3;
then FD is one-to-one by A1, A10, A12, A13, FINSEQ_4:63;
then A17: ex z being object st FD " {x} = {z} by A16, FUNCT_1:74;
FD " {x} = f " {x} by A15, STIRL2_1:54;
hence card (f " {x}) = 1 by A17, CARD_1:30; :: thesis: verum