let R be finite Skew-Field; :: thesis: for s being Element of R st s is Element of () holds
dim divides dim

let s be Element of R; :: thesis: ( s is Element of () implies dim divides dim )
assume A1: s is Element of () ; :: thesis:
set n = dim ;
set ns = dim ;
set q = card the carrier of ();
A2: dim in NAT by ORDINAL1:def 12;
A3: dim in NAT by ORDINAL1:def 12;
A4: 0 < dim by Th34;
A5: 1 < card the carrier of () by Th20;
0 < (card the carrier of ()) |^ () by PREPOWER:6;
then 0 + 1 < ((card the carrier of ()) |^ ()) + 1 by XREAL_1:8;
then A6: 1 <= (card the carrier of ()) |^ () by NAT_1:13;
0 < (card the carrier of ()) |^ () by PREPOWER:6;
then 0 + 1 < ((card the carrier of ()) |^ ()) + 1 by XREAL_1:8;
then 1 <= (card the carrier of ()) |^ () by NAT_1:13;
then A7: ((card the carrier of ()) |^ ()) - 1 = ((card the carrier of ()) |^ ()) -' 1 by XREAL_1:233;
((card the carrier of ()) |^ ()) - 1 = ((card the carrier of ()) |^ ()) -' 1 by ;
hence dim divides dim by A1, A2, A3, A4, A5, A7, Th3, Th35; :: thesis: verum