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 s' being Element of S such that
A2: ( s * s' = e & s' * s = e ) by A1;
A3: id E = LO ^ (1_ S) by Def1
.= LO ^ (s' * s) by A1, A2, GROUP_1:10
.= (LO ^ s') * (LO ^ s) by Def1 ;
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;
LO ^ s' in Funcs E,E by FUNCT_2:12;
then ex f being Function st
( LO ^ s' = f & dom f = E & rng f c= E ) by FUNCT_2:def 2;
hence LO ^ s is one-to-one by A3, A4, FUNCT_1:47; :: thesis: verum