let L1, L2 be non empty 1-sorted ; :: thesis: for g1 being Function of L1,L2
for g2 being Function of L2,L1 st g2 * g1 = id L1 holds
( g1 is one-to-one & g2 is onto )
let g1 be Function of L1,L2; :: thesis: for g2 being Function of L2,L1 st g2 * g1 = id L1 holds
( g1 is one-to-one & g2 is onto )
let g2 be Function of L2,L1; :: thesis: ( g2 * g1 = id L1 implies ( g1 is one-to-one & g2 is onto ) )
assume A1: g2 * g1 = id L1 ; :: thesis: ( g1 is one-to-one & g2 is onto )
hence g1 is one-to-one by FUNCT_2:29; :: thesis: g2 is onto
rng g2 = the carrier of L1 by A1, FUNCT_2:29;
hence g2 is onto by FUNCT_2:def 3; :: thesis: verum