let F be Field; :: thesis: for S being inducing_subfield Subset of F
for a, b being Element of F
for x, y being Element of (InducedSubfield S) st a = x & b = y holds
( a + b = x + y & a * b = x * y )
let S be inducing_subfield Subset of F; :: thesis: for a, b being Element of F
for x, y being Element of (InducedSubfield S) st a = x & b = y holds
( a + b = x + y & a * b = x * y )
let a, b be Element of F; :: thesis: for x, y being Element of (InducedSubfield S) st a = x & b = y holds
( a + b = x + y & a * b = x * y )
let x, y be Element of (InducedSubfield S); :: thesis: ( a = x & b = y implies ( a + b = x + y & a * b = x * y ) )
assume A1: ( a = x & b = y ) ; :: thesis: ( a + b = x + y & a * b = x * y )
set E = InducedSubfield S;
the carrier of (InducedSubfield S) = S by dis;
then A2: [x,y] in [:S,S:] by ZFMISC_1:def 2;
hence a + b = ( the addF of F || S) . (x,y) by A1, FUNCT_1:49
.= x + y by dis ;
:: thesis: a * b = x * y
thus a * b = ( the multF of F || S) . (x,y) by A1, A2, FUNCT_1:49
.= x * y by dis ; :: thesis: verum