let G be Group; :: thesis: for E being non empty set
for x, y being Element of E
for T being LeftOperation of G,E st x,y are_conjugated_under T holds
y,x are_conjugated_under T
let E be non empty set ; :: thesis: for x, y being Element of E
for T being LeftOperation of G,E st x,y are_conjugated_under T holds
y,x are_conjugated_under T
let x, y be Element of E; :: thesis: for T being LeftOperation of G,E st x,y are_conjugated_under T holds
y,x are_conjugated_under T
let T be LeftOperation of G,E; :: thesis: ( x,y are_conjugated_under T implies y,x are_conjugated_under T )
assume x,y are_conjugated_under T ; :: thesis: y,x are_conjugated_under T
then consider g being Element of G such that
A1: y = (T ^ g) . x by Def14;
x in E ;
then x in dom (T ^ g) by FUNCT_2:def 1;
then (T ^ (g ")) . y = ((T ^ (g ")) * (T ^ g)) . x by A1, FUNCT_1:13
.= (T ^ ((g ") * g)) . x by Def1
.= (T ^ (1_ G)) . x by GROUP_1:def 5
.= (id E) . x by Def1
.= x by FUNCT_1:18 ;
hence y,x are_conjugated_under T by Def14; :: thesis: verum