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 ;
suppose Fx in Y ; :: thesis: Fx in rng G
then Fx in rng F by ;
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 ;
hence Fx in rng G by ; :: 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 ;
then A23: F . x9 in rng F by FUNCT_1:def 3;
F . x9 = G . x9 by ;
hence ( x9 in dom F & F . x9 = G . x9 & G . x9 <> y ) by ; :: 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 ;
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 ;
A27: F . x2 = G . x2 by ;
x1 in dom F by ;
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 ;
hence x1 = x2 by ; :: thesis: verum
end;
suppose A29: ( x1 in {x} & x2 in X ) ; :: thesis: x1 = x2
then G . x1 = y by ;
hence x1 = x2 by ; :: 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 ; :: thesis: verum
end;
end;
end;
hence x1 = x2 ; :: thesis: verum
end;