H1: R is Subring of S by FIELD_4:def 1;
reconsider aR = a, bR = b as Element of R by FIELD_7:def 5;
[aR,bR] in [: the carrier of R, the carrier of R:] by ZFMISC_1:def 2;
then a * b = ( the multF of S || the carrier of R) . (a,b) by FUNCT_1:49
.= aR * bR by H1, C0SP1:def 3 ;
hence a * b is R -membered by FIELD_7:def 5; :: thesis: verum