let R be Field; :: thesis: for S being FieldExtension of R
for a, b being Element of S
for x, y being Element of (F_Alg S) st a = x & b = y holds
a * b = x * y
let S be FieldExtension of R; :: thesis: for a, b being Element of S
for x, y being Element of (F_Alg S) st a = x & b = y holds
a * b = x * y
let a, b be Element of S; :: thesis: for x, y being Element of (F_Alg S) st a = x & b = y holds
a * b = x * y
let x, y be Element of (F_Alg S); :: thesis: ( a = x & b = y implies a * b = x * y )
assume ( a = x & b = y ) ; :: thesis: a * b = x * y
hence a * b = ( the multF of S || the carrier of (F_Alg S)) . (x,y) by RING_3:1
.= x * y by d ;
:: thesis: verum