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 )

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

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

Y \/ {y} c= rng G

hence G is onto by FUNCT_2:def 3; :: thesis: verum

end;Y \/ {y} c= rng G

proof

then
Y \/ {y} = rng G
;
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

end;assume A5: Fx in Y \/ {y} ; :: thesis: Fx in rng G

now :: thesis: Fx in rng Gend;

hence
Fx in rng G
; :: thesis: verumper cases
( Fx in Y or Fx in {y} )
by A5, XBOOLE_0:def 3;

end;

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

hence G is onto by FUNCT_2:def 3; :: 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 )

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

now :: thesis: x1 = x2end;

hence
x1 = x2
; :: thesis: verumper 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;

end;

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