let R be Field; :: thesis: for E being FieldExtension of R
for a, b being Element of E
for x, y being Element of (F_Alg E) st a = x & b = y holds
a + b = x + y
let E be FieldExtension of R; :: thesis: for a, b being Element of E
for x, y being Element of (F_Alg E) 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_Alg E) st a = x & b = y holds
a + b = x + y
let x, y be Element of (F_Alg E); :: thesis: ( a = x & b = y implies a + b = x + y )
assume A1: ( a = x & b = y ) ; :: thesis: a + b = x + y
A2: the carrier of (F_Alg E) = Alg_El E by d;
hence a + b = ( the addF of E || (Alg_El E)) . (x,y) by A1, RING_3:1
.= x + y by d, A2 ;
:: thesis: verum