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 )

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, STIRL2_1:60;

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

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

then consider y being set such that
assume A5:
for y being set st y in Y holds

card (F " {y}) <= 1 ; :: thesis: contradiction

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

then
f is one-to-one
by A3, FUNCT_1:74;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;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

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

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, STIRL2_1:60;

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