let S be non empty unital multMagma ; :: thesis: for E being non empty set
for x, y, z being Element of E
for T being LeftOperation of S,E st x,y are_conjugated_under T & y,z are_conjugated_under T holds
x,z are_conjugated_under T
let E be non empty set ; :: thesis: for x, y, z being Element of E
for T being LeftOperation of S,E st x,y are_conjugated_under T & y,z are_conjugated_under T holds
x,z are_conjugated_under T
let x, y, z be Element of E; :: thesis: for T being LeftOperation of S,E st x,y are_conjugated_under T & y,z are_conjugated_under T holds
x,z are_conjugated_under T
let T be LeftOperation of S,E; :: thesis: ( x,y are_conjugated_under T & y,z are_conjugated_under T implies x,z are_conjugated_under T )
assume x,y are_conjugated_under T ; :: thesis: ( not y,z are_conjugated_under T or x,z are_conjugated_under T )
then consider s1 being Element of S such that
A1: y = (T ^ s1) . x ;
assume y,z are_conjugated_under T ; :: thesis: x,z are_conjugated_under T
then consider s2 being Element of S such that
A2: z = (T ^ s2) . y ;
x in E ;
then x in dom (T ^ s1) by FUNCT_2:def 1;
then z = ((T ^ s2) * (T ^ s1)) . x by A1, A2, FUNCT_1:13
.= (T ^ (s2 * s1)) . x by Def1 ;
hence x,z are_conjugated_under T ; :: thesis: verum