let G be set ; :: thesis: for H being non empty set
for h being Function of G,H
for g1 being Function of H,G st h is bijective & g1 = h " holds
g1 is bijective
let H be non empty set ; :: thesis: for h being Function of G,H
for g1 being Function of H,G st h is bijective & g1 = h " holds
g1 is bijective
let h be Function of G,H; :: thesis: for g1 being Function of H,G st h is bijective & g1 = h " holds
g1 is bijective
let g1 be Function of H,G; :: thesis: ( h is bijective & g1 = h " implies g1 is bijective )
assume A1: ( h is bijective & g1 = h " ) ; :: thesis: g1 is bijective
then ( dom h = G & rng g1 = dom h ) by FUNCT_1:33, FUNCT_2:def 1;
hence g1 is bijective by A1, FUNCT_2:def 3; :: thesis: verum