let X, Y, x, y be set ; :: thesis: ( ( Y is empty implies X is empty ) implies for F being Function of X,Y
for G being Function of (X \/ {x}),(Y \/ {y}) st G | X = F & G . x = y holds
( ( F is onto implies G is onto ) & ( not y in Y & F is one-to-one implies G is one-to-one ) ) )
assume A1: ( Y is empty implies X is empty ) ; :: thesis: for F being Function of X,Y
for G being Function of (X \/ {x}),(Y \/ {y}) st G | X = F & G . x = y holds
( ( F is onto implies G is onto ) & ( not y in Y & F is one-to-one implies G is one-to-one ) )
let F be Function of X,Y; :: thesis: for G being Function of (X \/ {x}),(Y \/ {y}) st G | X = F & G . x = y holds
( ( F is onto implies G is onto ) & ( not y in Y & F is one-to-one implies G is one-to-one ) )
let G be Function of (X \/ {x}),(Y \/ {y}); :: thesis: ( G | X = F & G . x = y implies ( ( F is onto implies G is onto ) & ( not y in Y & F is one-to-one implies G is one-to-one ) ) )
assume that
A2: G | X = F and
A3: G . x = y ; :: thesis: ( ( F is onto implies G is onto ) & ( not y in Y & F is one-to-one implies G is one-to-one ) )
thus ( F is onto implies G is onto ) :: thesis: ( not y in Y & F is one-to-one implies G is one-to-one )

proof

assume A4: F is onto ; :: thesis: G is onto
Y \/ {y} c= rng G

proof

let Fx be object ; :: according to TARSKI:def 3 :: thesis: ( not Fx in Y \/ {y} or Fx in rng G )
assume A5: Fx in Y \/ {y} ; :: thesis: Fx in rng G

now :: thesis: Fx in rng G

per cases ( Fx in Y or Fx in {y} ) by A5, XBOOLE_0:def 3;

suppose Fx in Y ; :: thesis: Fx in rng G

then Fx in rng F by A4, FUNCT_2:def 3;
then consider x9 being object such that
A6: x9 in dom F and
A7: F . x9 = Fx by FUNCT_1:def 3;
A8: x9 in X by A6;
A9: dom G = X \/ {x} by FUNCT_2:def 1;
A10: X c= X \/ {x} by XBOOLE_1:7;
G . x9 = F . x9 by A2, A6, FUNCT_1:47;
hence Fx in rng G by A7, A8, A10, A9, FUNCT_1:def 3; :: thesis: verum

end;

suppose A11: Fx in {y} ; :: thesis: Fx in rng G

A12: dom G = X \/ {x} by FUNCT_2:def 1;
A13: {x} c= X \/ {x} by XBOOLE_1:7;
A14: x in {x} by TARSKI:def 1;
Fx = y by A11, TARSKI:def 1;
hence Fx in rng G by A3, A12, A14, A13, FUNCT_1:def 3; :: thesis: verum

end;

end;

end;

hence Fx in rng G ; :: thesis: verum

end;

then Y \/ {y} = rng G ;
hence G is onto by FUNCT_2:def 3; :: thesis: verum

end;

thus ( not y in Y & F is one-to-one implies G is one-to-one ) :: thesis: verum

proof

assume that
A15: not y in Y and
A16: F is one-to-one ; :: thesis: G is one-to-one
let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in dom G or not x2 in dom G or not G . x1 = G . x2 or x1 = x2 )
assume that
A17: x1 in dom G and
A18: x2 in dom G and
A19: G . x1 = G . x2 ; :: thesis: x1 = x2
A20: for x9 being set st x9 in X holds
( x9 in dom F & F . x9 = G . x9 & G . x9 <> y )

proof

let x9 be set ; :: thesis: ( x9 in X implies ( x9 in dom F & F . x9 = G . x9 & G . x9 <> y ) )
assume A21: x9 in X ; :: thesis: ( x9 in dom F & F . x9 = G . x9 & G . x9 <> y )
A22: x9 in dom F by A1, A21, FUNCT_2:def 1;
then A23: F . x9 in rng F by FUNCT_1:def 3;
F . x9 = G . x9 by A2, A22, FUNCT_1:47;
hence ( x9 in dom F & F . x9 = G . x9 & G . x9 <> y ) by A15, A21, A23, FUNCT_2:def 1; :: thesis: verum

end;

now :: thesis: x1 = x2

per cases ( ( x1 in X & x2 in X ) or ( x1 in X & x2 in {x} ) or ( x1 in {x} & x2 in X ) or ( x1 in {x} & x2 in {x} ) ) by A17, A18, XBOOLE_0:def 3;

suppose A24: ( x1 in X & x2 in X ) ; :: thesis: x1 = x2

then A25: F . x1 = G . x1 by A20;
A26: x2 in dom F by A20, A24;
A27: F . x2 = G . x2 by A20, A24;
x1 in dom F by A20, A24;
hence x1 = x2 by A16, A19, A26, A25, A27; :: thesis: verum

end;

suppose A28: ( x1 in X & x2 in {x} ) ; :: thesis: x1 = x2

then G . x2 = y by A3, TARSKI:def 1;
hence x1 = x2 by A19, A20, A28; :: thesis: verum

end;

suppose A29: ( x1 in {x} & x2 in X ) ; :: thesis: x1 = x2

then G . x1 = y by A3, TARSKI:def 1;
hence x1 = x2 by A19, A20, A29; :: thesis: verum

end;

suppose A30: ( x1 in {x} & x2 in {x} ) ; :: thesis: x1 = x2

then x = x1 by TARSKI:def 1;
hence x1 = x2 by A30, TARSKI:def 1; :: thesis: verum

end;

end;

end;

hence x1 = x2 ; :: thesis: verum

end;