let X, Y be non empty set ; :: thesis: for f being Function of X,Y st f is bijective holds
for y being Element of Y holds f . ((f ") . y) = y
let f be Function of X,Y; :: thesis: ( f is bijective implies for y being Element of Y holds f . ((f ") . y) = y )
assume A1: f is bijective ; :: thesis: for y being Element of Y holds f . ((f ") . y) = y
let y be Element of Y; :: thesis: f . ((f ") . y) = y
f is onto by A1;
then reconsider g = f " as Function of Y,X by A1, FUNCT_2:25;
y = (g ") . (g . y) by A1, FUNCT_2:26
.= f . ((f ") . y) by A1, FUNCT_1:43 ;
hence f . ((f ") . y) = y ; :: thesis: verum