let E be non empty set ; :: thesis: for S being non empty Group-like multMagma
for s being Element of
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
for LO being LeftOperation of S,E holds LO ^ s is one-to-one
let s be Element of ; :: 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 such that
A1: for h being Element of holds
( h * e = h & e * h = h & ex g being Element of st
( h * g = e & g * h = e ) ) by GROUP_1:def 3;
consider s' being Element of such that
s * s' = e and
A2: s' * s = e by A1;
LO ^ s' in Funcs E,E by FUNCT_2:12;
then A3: 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 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 ^ (s' * s) by A1, A2, GROUP_1:10
.= (LO ^ s') * (LO ^ s) by Def1 ;
hence LO ^ s is one-to-one by A4, A3, FUNCT_1:47; :: thesis: verum