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

( 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