let S be non empty unital multMagma ; :: thesis: for E being non empty finite set
for x being Element of E
for T being LeftOperation of S,E st x is_fixed_under T holds
the_orbit_of x,T = {x}
let E be non empty finite set ; :: thesis: for x being Element of E
for T being LeftOperation of S,E st x is_fixed_under T holds
the_orbit_of x,T = {x}
let x be Element of E; :: thesis: for T being LeftOperation of S,E st x is_fixed_under T holds
the_orbit_of x,T = {x}
let T be LeftOperation of S,E; :: thesis: ( x is_fixed_under T implies the_orbit_of x,T = {x} )
set X = the_orbit_of x,T;
assume A1:
x is_fixed_under T
; :: thesis: the_orbit_of x,T = {x}
now assume
the_orbit_of x,
T <> {x}
;
:: thesis: contradictionthen A2:
not for
x' being
set holds
(
x' in the_orbit_of x,
T iff
x' = x )
by TARSKI:def 1;
the_orbit_of x,
T <> {}
by Th7;
then
ex
x' being
set st
x' in the_orbit_of x,
T
by XBOOLE_0:def 1;
then consider x'' being
set such that A3:
x'' <> x
and A4:
x'' in the_orbit_of x,
T
by A2;
consider y' being
Element of
E such that A5:
x'' = y'
and A6:
x,
y' are_conjugated_under T
by A4;
ex
s being
Element of
S st
y' = (T ^ s) . x
by A6, Def14;
hence
contradiction
by A1, A3, A5, Def12;
:: thesis: verum end;
hence
the_orbit_of x,T = {x}
; :: thesis: verum