let S be non empty unital multMagma ; :: thesis: for E being non empty set
for x being Element of E
for T being LeftOperation of S,E holds x,x are_conjugated_under T
let E be non empty set ; :: thesis: for x being Element of E
for T being LeftOperation of S,E holds x,x are_conjugated_under T
let x be Element of E; :: thesis: for T being LeftOperation of S,E holds x,x are_conjugated_under T
let T be LeftOperation of S,E; :: thesis: x,x are_conjugated_under T
x = (id E) . x
.= (T ^ (1_ S)) . x by Def1 ;
hence x,x are_conjugated_under T ; :: thesis: verum