let F be strict Field; :: thesis: for p being linear Element of the carrier of (Polynom-Ring F) holds embField (emb p) = F

let p be linear Element of the carrier of (Polynom-Ring F); :: thesis: embField (emb p) = F

set FP = embField (emb p);

set f = emb p;

set K = (Polynom-Ring F) / ({p} -Ideal);

X: ( [#] ((Polynom-Ring F) / ({p} -Ideal)) = the carrier of ((Polynom-Ring F) / ({p} -Ideal)) & [#] F = the carrier of F ) ;

H: the carrier of F = the carrier of (embField (emb p)) by polyd1;

A: ( 1. (embField (emb p)) = 1. F & 0. (embField (emb p)) = 0. F ) by FIELD_2:def 7;

B: dom the addF of (embField (emb p)) = [: the carrier of (embField (emb p)), the carrier of (embField (emb p)):] by FUNCT_2:def 1

.= dom the addF of F by H, FUNCT_2:def 1 ;

B: dom the multF of (embField (emb p)) = [: the carrier of (embField (emb p)), the carrier of (embField (emb p)):] by FUNCT_2:def 1

.= dom the multF of F by H, FUNCT_2:def 1 ;

hence embField (emb p) = F by A, C, polyd1; :: thesis: verum

let p be linear Element of the carrier of (Polynom-Ring F); :: thesis: embField (emb p) = F

set FP = embField (emb p);

set f = emb p;

set K = (Polynom-Ring F) / ({p} -Ideal);

X: ( [#] ((Polynom-Ring F) / ({p} -Ideal)) = the carrier of ((Polynom-Ring F) / ({p} -Ideal)) & [#] F = the carrier of F ) ;

H: the carrier of F = the carrier of (embField (emb p)) by polyd1;

A: ( 1. (embField (emb p)) = 1. F & 0. (embField (emb p)) = 0. F ) by FIELD_2:def 7;

B: dom the addF of (embField (emb p)) = [: the carrier of (embField (emb p)), the carrier of (embField (emb p)):] by FUNCT_2:def 1

.= dom the addF of F by H, FUNCT_2:def 1 ;

now :: thesis: for x being Element of dom the addF of F holds the addF of (embField (emb p)) . x = the addF of F . x

then C:
the addF of (embField (emb p)) = the addF of F
by B;let x be Element of dom the addF of F; :: thesis: the addF of (embField (emb p)) . x = the addF of F . x

consider o being Element of [: the carrier of F, the carrier of F:] such that

B1: x = o ;

consider a, b being object such that

B2: ( a in the carrier of F & b in the carrier of F & o = [a,b] ) by ZFMISC_1:def 2;

( a in ( the carrier of ((Polynom-Ring F) / ({p} -Ideal)) \ (rng (emb p))) \/ the carrier of F & b in ( the carrier of ((Polynom-Ring F) / ({p} -Ideal)) \ (rng (emb p))) \/ the carrier of F ) by B2, XBOOLE_0:def 3;

then reconsider a = a, b = b as Element of carr (emb p) by X, FIELD_2:def 2;

thus the addF of (embField (emb p)) . x = (addemb (emb p)) . (a,b) by B1, B2, FIELD_2:def 7

.= addemb ((emb p),a,b) by FIELD_2:def 4

.= the addF of F . (a,b) by B2, X, FIELD_2:def 3

.= the addF of F . x by B1, B2 ; :: thesis: verum

end;consider o being Element of [: the carrier of F, the carrier of F:] such that

B1: x = o ;

consider a, b being object such that

B2: ( a in the carrier of F & b in the carrier of F & o = [a,b] ) by ZFMISC_1:def 2;

( a in ( the carrier of ((Polynom-Ring F) / ({p} -Ideal)) \ (rng (emb p))) \/ the carrier of F & b in ( the carrier of ((Polynom-Ring F) / ({p} -Ideal)) \ (rng (emb p))) \/ the carrier of F ) by B2, XBOOLE_0:def 3;

then reconsider a = a, b = b as Element of carr (emb p) by X, FIELD_2:def 2;

thus the addF of (embField (emb p)) . x = (addemb (emb p)) . (a,b) by B1, B2, FIELD_2:def 7

.= addemb ((emb p),a,b) by FIELD_2:def 4

.= the addF of F . (a,b) by B2, X, FIELD_2:def 3

.= the addF of F . x by B1, B2 ; :: thesis: verum

B: dom the multF of (embField (emb p)) = [: the carrier of (embField (emb p)), the carrier of (embField (emb p)):] by FUNCT_2:def 1

.= dom the multF of F by H, FUNCT_2:def 1 ;

now :: thesis: for x being Element of dom the multF of F holds the multF of (embField (emb p)) . x = the multF of F . x

then
the multF of (embField (emb p)) = the multF of F
by B;let x be Element of dom the multF of F; :: thesis: the multF of (embField (emb p)) . x = the multF of F . x

consider o being Element of [: the carrier of F, the carrier of F:] such that

B1: x = o ;

consider a, b being object such that

B2: ( a in the carrier of F & b in the carrier of F & o = [a,b] ) by ZFMISC_1:def 2;

( a in ( the carrier of ((Polynom-Ring F) / ({p} -Ideal)) \ (rng (emb p))) \/ the carrier of F & b in ( the carrier of ((Polynom-Ring F) / ({p} -Ideal)) \ (rng (emb p))) \/ the carrier of F ) by B2, XBOOLE_0:def 3;

then reconsider a = a, b = b as Element of carr (emb p) by X, FIELD_2:def 2;

thus the multF of (embField (emb p)) . x = (multemb (emb p)) . (a,b) by B1, B2, FIELD_2:def 7

.= multemb ((emb p),a,b) by FIELD_2:def 6

.= the multF of F . (a,b) by B2, X, FIELD_2:def 5

.= the multF of F . x by B1, B2 ; :: thesis: verum

end;consider o being Element of [: the carrier of F, the carrier of F:] such that

B1: x = o ;

consider a, b being object such that

B2: ( a in the carrier of F & b in the carrier of F & o = [a,b] ) by ZFMISC_1:def 2;

( a in ( the carrier of ((Polynom-Ring F) / ({p} -Ideal)) \ (rng (emb p))) \/ the carrier of F & b in ( the carrier of ((Polynom-Ring F) / ({p} -Ideal)) \ (rng (emb p))) \/ the carrier of F ) by B2, XBOOLE_0:def 3;

then reconsider a = a, b = b as Element of carr (emb p) by X, FIELD_2:def 2;

thus the multF of (embField (emb p)) . x = (multemb (emb p)) . (a,b) by B1, B2, FIELD_2:def 7

.= multemb ((emb p),a,b) by FIELD_2:def 6

.= the multF of F . (a,b) by B2, X, FIELD_2:def 5

.= the multF of F . x by B1, B2 ; :: thesis: verum

hence embField (emb p) = F by A, C, polyd1; :: thesis: verum