consider e being Element of S such that
A1: for h being Element of S holds
( h * e = h & e * h = h & ex g being Element of S st
( h * g = e & g * h = e ) ) by GROUP_1:def 2;
consider s9 being Element of S such that
s * s9 = e and
A2: s9 * s = e by A1;
LO ^ s9 in Funcs (E,E) by FUNCT_2:9;
then A3: ex f being Function st
( LO ^ s9 = f & dom f = E & rng f c= E ) by FUNCT_2:def 2;
LO ^ s in Funcs (E,E) by FUNCT_2:9;
then A4: ex f being Function st
( LO ^ s = f & dom f = E & rng f c= E ) by FUNCT_2:def 2;
id E = LO ^ (1_ S) by Def1
.= LO ^ (s9 * s) by A1, A2, GROUP_1:4
.= (LO ^ s9) * (LO ^ s) by Def1 ;
hence for b₁ being Function of E,E st b₁ = LO ^ s holds
b₁ is one-to-one by A4, A3, FUNCT_1:25; :: thesis: verum