let X, Y be non empty set ; for f being Function of X,Y
for g being Function of Y,X st ( for x being Element of X holds g . (f . x) = x ) & ( for y being Element of Y holds f . (g . y) = y ) holds
( f is one-to-one & f is onto & g is one-to-one & g is onto & g = f " & f = g " )
let f be Function of X,Y; for g being Function of Y,X st ( for x being Element of X holds g . (f . x) = x ) & ( for y being Element of Y holds f . (g . y) = y ) holds
( f is one-to-one & f is onto & g is one-to-one & g is onto & g = f " & f = g " )
let g be Function of Y,X; ( ( for x being Element of X holds g . (f . x) = x ) & ( for y being Element of Y holds f . (g . y) = y ) implies ( f is one-to-one & f is onto & g is one-to-one & g is onto & g = f " & f = g " ) )
assume A1:
for x being Element of X holds g . (f . x) = x
; ( ex y being Element of Y st not f . (g . y) = y or ( f is one-to-one & f is onto & g is one-to-one & g is onto & g = f " & f = g " ) )
assume A2:
for y being Element of Y holds f . (g . y) = y
; ( f is one-to-one & f is onto & g is one-to-one & g is onto & g = f " & f = g " )
then P2:
g * f = id X
by FUNCT_2:124;
then P4:
f * g = id Y
by FUNCT_2:124;
thus P5:
( f is one-to-one & f is onto )
by P2, P4, FUNCT_2:23; ( g is one-to-one & g is onto & g = f " & f = g " )
thus P6:
( g is one-to-one & g is onto )
by P2, P4, FUNCT_2:23; ( g = f " & f = g " )
rng f = Y
by P5, FUNCT_2:def 3;
hence
g = f "
by FUNCT_2:30, P2, FUNCT_2:23; f = g "
rng g = X
by P6, FUNCT_2:def 3;
hence
f = g "
by FUNCT_2:30, P4, FUNCT_2:23; verum