let R be finite Skew-Field; :: thesis: for r being Element of R st r is Element of () holds
((card the carrier of ()) |^ ()) - 1 divides ((card the carrier of ()) |^ ()) - 1

let r be Element of R; :: thesis: ( r is Element of () implies ((card the carrier of ()) |^ ()) - 1 divides ((card the carrier of ()) |^ ()) - 1 )
assume A1: r is Element of () ; :: thesis: ((card the carrier of ()) |^ ()) - 1 divides ((card the carrier of ()) |^ ()) - 1
set G = MultGroup R;
set q = card the carrier of ();
set qr = card the carrier of ();
set n = dim ;
reconsider s = r as Element of () by A1;
card R = (card the carrier of ()) |^ () by Th31;
then card () = ((card the carrier of ()) |^ ()) - 1 by UNIROOTS:18;
then ((card the carrier of ()) |^ ()) - 1 = (card ()) * (card ()) by Th13;
then card () divides ((card the carrier of ()) |^ ()) - 1 by INT_1:def 3;
then (card the carrier of ()) - 1 divides ((card the carrier of ()) |^ ()) - 1 by Th30;
hence ((card the carrier of ()) |^ ()) - 1 divides ((card the carrier of ()) |^ ()) - 1 by Th33; :: thesis: verum