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 ;
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 ;
then card (F " {y}) = 1 by ;
hence ex x being object st F " {y} = {x} by CARD_2:42; :: thesis: verum
end;
then f is one-to-one by ;
then X,Y are_equipotent by ;
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 ;
dom (F | ((dom f) \ (F " {y}))) = (dom f) \ (F " {y}) by ;
then A10: card (dom (F | ((dom f) \ (F " {y})))) = (card XX) - (card (F " {y})) by ;
set Yy = Y \ {y};
A11: rng (F | ((dom f) \ (F " {y}))) = Y \ {y} by ;
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 ;
then Segm c1 c= Segm (card (dom (F | ((dom f) \ (F " {y}))))) by ;
then (card Y) + (- 1) <= (card Y) + (1 - (card (F " {y}))) by ;
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 ; :: 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 ;
FD is onto by ;
then FD is one-to-one by ;
then A17: ex z being object st FD " {x} = {z} by ;
FD " {x} = f " {x} by ;
hence card (f " {x}) = 1 by ; :: thesis: verum