let X, Y be non empty set ; :: thesis: for f being Function of X,Y st f is bijective holds
ex g being Function of Y,X st
( g is bijective & g = f " & .: g = (.: f) " )
let f be Function of X,Y; :: thesis: ( f is bijective implies ex g being Function of Y,X st
( g is bijective & g = f " & .: g = (.: f) " ) )
assume A1: f is bijective ; :: thesis: ex g being Function of Y,X st
( g is bijective & g = f " & .: g = (.: f) " )
then A2: ( rng f = dom (f ") & dom f = rng (f ") ) by FUNCT_1:33;
A3: ( dom f = X & rng f = Y ) by A1, FUNCT_2:def 1, FUNCT_2:def 3;
then reconsider g = f " as Function of Y,X by A2, FUNCT_2:1;
take g ; :: thesis: ( g is bijective & g = f " & .: g = (.: f) " )
A4: g is onto by A2, A3, FUNCT_2:def 3;
hence g is bijective by A1; :: thesis: ( g = f " & .: g = (.: f) " )
thus g = f " ; :: thesis: .: g = (.: f) "
.: f is bijective by A1, Th1;
then A5: ( dom (.: f) = bool X & rng (.: f) = bool Y ) by FUNCT_2:def 1, FUNCT_2:def 3;
.: g is bijective by A1, A4, Th1;
then A6: ( dom (.: g) = bool Y & rng (.: g) = bool X ) by FUNCT_2:def 1, FUNCT_2:def 3;
for x, y being object st x in dom (.: f) & y in dom (.: g) holds
( (.: f) . x = y iff (.: g) . y = x )

proof

let x, y be object ; :: thesis: ( x in dom (.: f) & y in dom (.: g) implies ( (.: f) . x = y iff (.: g) . y = x ) )
assume A7: ( x in dom (.: f) & y in dom (.: g) ) ; :: thesis: ( (.: f) . x = y iff (.: g) . y = x )
then reconsider s = x as Subset of X ;
reconsider t = y as Subset of Y by A7;

now :: thesis: ( (.: f) . x = y implies (.: g) . y = x )

assume (.: f) . x = y ; :: thesis: (.: g) . y = x
then y = f .: s by A1, Th1;
then (.: g) . y = g .: (f .: s) by A1, A4, Th1;
then (.: g) . y = f " (f .: s) by FUNCT_1:85, A1;
hence (.: g) . y = x by A1, A3, FUNCT_1:94; :: thesis: verum

end;

hence ( (.: f) . x = y implies (.: g) . y = x ) ; :: thesis: ( (.: g) . y = x implies (.: f) . x = y )
assume (.: g) . y = x ; :: thesis: (.: f) . x = y
then x = g .: t by A1, A4, Th1;
then (.: f) . x = f .: (g .: t) by A1, Th1;
then (.: f) . x = (g ") .: (g .: t) by FUNCT_1:43, A1;
then (.: f) . x = g " (g .: t) by A1, FUNCT_1:85;
hence (.: f) . x = y by A1, A2, A3, FUNCT_1:94; :: thesis: verum

end;

hence .: g = (.: f) " by A1, A5, A6, FUNCT_1:38; :: thesis: verum