let R be Ring; :: thesis: for R being Subring of R
for x, y being Element of R
for x1, y1 being Element of R st x = x1 & y = y1 holds
x * y = x1 * y1
let S be Subring of R; :: thesis: for x, y being Element of R
for x1, y1 being Element of S st x = x1 & y = y1 holds
x * y = x1 * y1
let x, y be Element of R; :: thesis: for x1, y1 being Element of S st x = x1 & y = y1 holds
x * y = x1 * y1
let x1, y1 be Element of S; :: thesis: ( x = x1 & y = y1 implies x * y = x1 * y1 )
set C1 = the carrier of S;
the multF of S = the multF of R || the carrier of S by C0SP1:def 3;
hence ( x = x1 & y = y1 implies x * y = x1 * y1 ) by FUNCT_1:49, ZFMISC_1:87; :: thesis: verum