let X, Y, x, y be set ; ( ( 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 )
; 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; 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}); ( 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
; ( ( 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 )
( not y in Y & F is one-to-one implies G is one-to-one )
thus
( not y in Y & F is one-to-one implies G is one-to-one )
verum