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