let F be Field; :: thesis: for a, b being Element of F
for x, y being Element of (PrimeField F) st a = x & b = y holds
a + b = x + y
let a, b be Element of F; :: thesis: for x, y being Element of (PrimeField F) st a = x & b = y holds
a + b = x + y
let x, y be Element of (PrimeField F); :: thesis: ( a = x & b = y implies a + b = x + y )
assume A1: ( a = x & b = y ) ; :: thesis: a + b = x + y
the carrier of (PrimeField F) = carrier/\ F by Def10;
hence a + b = ( the addF of F || (carrier/\ F)) . (x,y) by A1, Th1
.= x + y by Def10 ;
:: thesis: verum