let R be finite Skew-Field; :: thesis: for s being Element of R holds 1 < card the carrier of (centralizer s)

let s be Element of R; :: thesis: 1 < card the carrier of (centralizer s)

A1: card {(0. R),(1. R)} = 2 by CARD_2:57;

A2: 0. R is Element of (centralizer s) by Th27;

1_ R is Element of (centralizer s) by Th27;

then {(0. R),(1_ R)} c= the carrier of (centralizer s) by A2, ZFMISC_1:32;

then 2 <= card the carrier of (centralizer s) by A1, NAT_1:43;

hence 1 < card the carrier of (centralizer s) by XXREAL_0:2; :: thesis: verum

let s be Element of R; :: thesis: 1 < card the carrier of (centralizer s)

A1: card {(0. R),(1. R)} = 2 by CARD_2:57;

A2: 0. R is Element of (centralizer s) by Th27;

1_ R is Element of (centralizer s) by Th27;

then {(0. R),(1_ R)} c= the carrier of (centralizer s) by A2, ZFMISC_1:32;

then 2 <= card the carrier of (centralizer s) by A1, NAT_1:43;

hence 1 < card the carrier of (centralizer s) by XXREAL_0:2; :: thesis: verum