let E be non empty set ; :: thesis: for S being non empty Group-like multMagma
for s being Element of S
for LO being LeftOperation of S,E holds LO ^ s is one-to-one
let S be non empty Group-like multMagma ; :: thesis: for s being Element of S
for LO being LeftOperation of S,E holds LO ^ s is one-to-one
let s be Element of S; :: thesis: for LO being LeftOperation of S,E holds LO ^ s is one-to-one
let LO be LeftOperation of S,E; :: thesis: LO ^ s is one-to-one
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 3;
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:12;
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:12;
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:10
.= (LO ^ s9) * (LO ^ s) by Def1 ;
hence LO ^ s is one-to-one by A4, A3, FUNCT_1:47; :: thesis: verum