let R be Ring; :: thesis: for E being RingExtension of R
for a, b being Element of E
for x, y being Element of R st a = x & b = y holds
a * b = x * y
let E be RingExtension of R; :: thesis: for a, b being Element of E
for x, y being Element of R st a = x & b = y holds
a * b = x * y
let a, b be Element of E; :: thesis: for x, y being Element of R st a = x & b = y holds
a * b = x * y
let x, y be Element of R; :: thesis: ( a = x & b = y implies a * b = x * y )
assume A1: ( a = x & b = y ) ; :: thesis: a * b = x * y
A2: R is Subring of E by Def1;
A3: [x,y] in [: the carrier of R, the carrier of R:] by ZFMISC_1:def 2;
thus x * y = ( the multF of E || the carrier of R) . (x,y) by A2, C0SP1:def 3
.= a * b by A1, A3, FUNCT_1:49 ; :: thesis: verum