let R be finite Skew-Field; :: thesis: ( card the carrier of () = card the carrier of R iff R is commutative )
set X = the carrier of R;
set Y = the carrier of ();
hereby :: thesis: ( R is commutative implies card the carrier of () = card the carrier of R )
assume A1: card the carrier of R = card the carrier of () ; :: thesis: R is commutative
A2: the carrier of () c= the carrier of R by Th16;
card ( the carrier of R \ the carrier of ()) = (card the carrier of R) - (card the carrier of R) by ;
then the carrier of R \ the carrier of () = {} ;
then the carrier of R c= the carrier of () by XBOOLE_1:37;
then A3: the carrier of R = the carrier of () by ;
for x, s being Element of the carrier of R holds x * s = s * x by ;
hence R is commutative ; :: thesis: verum
end;
now :: thesis: ( R is commutative implies card the carrier of () = card the carrier of R )
assume A4: R is commutative ; :: thesis: card the carrier of () = card the carrier of R
for x being object st x in the carrier of R holds
x in the carrier of ()
proof
let x be object ; :: thesis: ( x in the carrier of R implies x in the carrier of () )
assume A5: x in the carrier of R ; :: thesis: x in the carrier of ()
for x being Element of the carrier of R holds x is Element of the carrier of ()
proof
let x be Element of the carrier of R; :: thesis: x is Element of the carrier of ()
for y being Element of the carrier of R holds x * y = y * x by A4;
then x in center R by Th17;
hence x is Element of the carrier of () ; :: thesis: verum
end;
then x is Element of the carrier of () by A5;
hence x in the carrier of () ; :: thesis: verum
end;
then A6: the carrier of R c= the carrier of () ;
the carrier of () c= the carrier of R by Th16;
hence card the carrier of () = card the carrier of R by ; :: thesis: verum
end;
hence ( R is commutative implies card the carrier of () = card the carrier of R ) ; :: thesis: verum