let R be Skew-Field; :: thesis: for s being Element of holds
( 0. R is Element of & 1_ R is Element of )
let s be Element of ; :: thesis: ( 0. R is Element of & 1_ R is Element of )
A1: 0. R = 0. (centralizer s) by Def5;
1. (centralizer s) = 1_ R by Def5;
hence ( 0. R is Element of & 1_ R is Element of ) by A1; :: thesis: verum