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 :: thesis: not the_orbit_of (x,T) <> {x}
assume the_orbit_of (x,T) <> {x} ; :: thesis: contradiction
then A2: not for x9 being object holds
( x9 in the_orbit_of (x,T) iff x9 = x ) by TARSKI:def 1;
ex x9 being object st x9 in the_orbit_of (x,T) by XBOOLE_0:def 1;
then consider x99 being set such that
A3: x99 <> x and
A4: x99 in the_orbit_of (x,T) by A2;
consider y9 being Element of E such that
A5: x99 = y9 and
A6: x,y9 are_conjugated_under T by A4;
ex s being Element of S st y9 = (T ^ s) . x by A6;
hence contradiction by A1, A3, A5; :: thesis: verum
end;
hence the_orbit_of (x,T) = {x} ; :: thesis: verum