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