let R be Ring; :: thesis: R is Subring of R
thus the carrier of R c= the carrier of R ; :: according to C0SP1:def 3 :: thesis: ( the addF of R = K754( the addF of R, the carrier of R) & the multF of R = K754( the multF of R, the carrier of R) & 1. R = 1. R & 0. R = 0. R )
thus ( the addF of R = K754( the addF of R, the carrier of R) & the multF of R = K754( the multF of R, the carrier of R) & 1. R = 1. R & 0. R = 0. R ) ; :: thesis: verum