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 set ; :: 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

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 x' being set such that
A6: ( x' in dom F & F . x' = Fx ) by FUNCT_1:def 5;
( x' in X & X c= X \/ {x} & dom G = X \/ {x} ) by A6, FUNCT_2:def 1, XBOOLE_1:7;
then ( x' in dom G & G . x' = F . x' ) by A2, A6, FUNCT_1:70;
hence Fx in rng G by A6, FUNCT_1:def 5; :: thesis: verum

end;

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

then ( Fx = y & dom G = X \/ {x} & x in {x} & {x} c= X \/ {x} ) by FUNCT_2:def 1, TARSKI:def 1, XBOOLE_1:7;
hence Fx in rng G by A3, FUNCT_1:def 5; :: thesis: verum

end;

end;

end;

hence Fx in rng G ; :: thesis: verum

end;

then Y \/ {y} = rng G by XBOOLE_0:def 10;
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 A7: ( not y in Y & F is one-to-one ) ; :: thesis: G is one-to-one
let x1, x2 be set ; :: according to FUNCT_1:def 8 :: thesis: ( not x1 in dom G or not x2 in dom G or not G . x1 = G . x2 or x1 = x2 )
assume A8: ( x1 in dom G & x2 in dom G & G . x1 = G . x2 ) ; :: thesis: x1 = x2
A9: for x' being set st x' in X holds
( x' in dom F & F . x' = G . x' & G . x' <> y )

proof

let x' be set ; :: thesis: ( x' in X implies ( x' in dom F & F . x' = G . x' & G . x' <> y ) )
assume A10: x' in X ; :: thesis: ( x' in dom F & F . x' = G . x' & G . x' <> y )
x' in dom F by A1, A10, FUNCT_2:def 1;
then ( F . x' = G . x' & F . x' in rng F ) by A2, FUNCT_1:70, FUNCT_1:def 5;
hence ( x' in dom F & F . x' = G . x' & G . x' <> y ) by A7, A10, FUNCT_2:def 1; :: thesis: verum

end;

now

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 A8, XBOOLE_0:def 3;

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

then ( x1 in dom F & x2 in dom F & F . x1 = G . x1 & F . x2 = G . x2 ) by A9;
hence x1 = x2 by A7, A8, FUNCT_1:def 8; :: thesis: verum

end;

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

then ( G . x2 = y & G . x1 <> y ) by A3, A9, TARSKI:def 1;
hence x1 = x2 by A8; :: thesis: verum

end;

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

then ( G . x1 = y & G . x2 <> y ) by A3, A9, TARSKI:def 1;
hence x1 = x2 by A8; :: thesis: verum

end;

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

then ( x = x1 & x = x2 ) by TARSKI:def 1;
hence x1 = x2 ; :: thesis: verum

end;

end;

end;

hence x1 = x2 ; :: thesis: verum

end;