let R be finite Skew-Field; :: thesis: 1 < card the carrier of (center R)
A1: card {(0. R),(1. R)} = 2 by CARD_2:76;
0. R in center R by Th19;
then A2: 0. R in the carrier of (center R) by STRUCT_0:def 5;
for s being Element of R holds (1. R) * s = s * (1. R)

proof

let s be Element of R; :: thesis: (1. R) * s = s * (1. R)
s * (1. R) = s by VECTSP_1:def 13
.= (1. R) * s by VECTSP_1:def 19 ;
hence (1. R) * s = s * (1. R) ; :: thesis: verum

end;

then 1. R in center R by Th18;
then 1. R in the carrier of (center R) by STRUCT_0:def 5;
then {(0. R),(1. R)} c= the carrier of (center R) by A2, ZFMISC_1:38;
then 2 <= card the carrier of (center R) by A1, NAT_1:44;
hence 1 < card the carrier of (center R) by XXREAL_0:2; :: thesis: verum