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} )
assume A1:
x is_fixed_under T
; :: thesis: the_orbit_of x,T = {x}
set X = the_orbit_of x,T;
now
the_orbit_of x,
T <> {}
by Th7;
then A2:
ex
x' being
set st
x' in the_orbit_of x,
T
by XBOOLE_0:def 1;
assume
the_orbit_of x,
T <> {x}
;
:: thesis: contradictionthen
not for
x' being
set holds
(
x' in the_orbit_of x,
T iff
x' = x )
by TARSKI:def 1;
then consider x'' being
set such that A3:
(
x'' <> x &
x'' in the_orbit_of x,
T )
by A2;
consider y' being
Element of
E such that A4:
(
x'' = y' &
x,
y' are_conjugated_under T )
by A3;
ex
s being
Element of
S st
y' = (T ^ s) . x
by A4, Def14;
hence
contradiction
by A1, A3, A4, Def12;
:: thesis: verum end;
hence
the_orbit_of x,T = {x}
; :: thesis: verum