let X, Y be non empty set ; :: thesis: 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; :: thesis: 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; :: thesis: ( ( 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 ; :: thesis: ( 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 ; :: thesis: ( f is one-to-one & f is onto & g is one-to-one & g is onto & g = f " & f = g " )

now :: thesis: for x being Element of X holds (g * f) . x = x

let x be Element of X; :: thesis: (g * f) . x = x
thus (g * f) . x = g . (f . x) by FUNCT_2:15
.= x by A1 ; :: thesis: verum

end;

then P2: g * f = id X by FUNCT_2:124;

now :: thesis: for y being Element of Y holds (f * g) . y = y

let y be Element of Y; :: thesis: (f * g) . y = y
thus (f * g) . y = f . (g . y) by FUNCT_2:15
.= y by A2 ; :: thesis: verum

end;

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; :: thesis: ( 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; :: thesis: ( g = f " & f = g " )
rng f = Y by P5, FUNCT_2:def 3;
hence g = f " by FUNCT_2:30, P2, FUNCT_2:23; :: thesis: f = g "
rng g = X by P6, FUNCT_2:def 3;
hence f = g " by FUNCT_2:30, P4, FUNCT_2:23; :: thesis: verum