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: contradiction
then A2: not for x9 being set holds
( x9 in the_orbit_of x,T iff x9 = x ) by TARSKI:def 1;
the_orbit_of x,T <> {} by Th7;
then ex x9 being set 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, Def14;
hence contradiction by A1, A3, A5, Def12; :: thesis: verum

end;

hence the_orbit_of x,T = {x} ; :: thesis: verum