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

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

set FP = embField (canHomP p);

set f = canHomP p;

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

H: the carrier of F = the carrier of (embField (canHomP p)) by polyd;

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

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

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

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

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

hence embField (canHomP p) = F by A, C, polyd; :: thesis: verum

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

set FP = embField (canHomP p);

set f = canHomP p;

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

H: the carrier of F = the carrier of (embField (canHomP p)) by polyd;

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

B: dom the addF of (embField (canHomP p)) = [: the carrier of (embField (canHomP p)), the carrier of (embField (canHomP 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 (canHomP p)) . x = the addF of F . x

then C:
the addF of (embField (canHomP p)) = the addF of F
by B;let x be Element of dom the addF of F; :: thesis: the addF of (embField (canHomP 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 p) \ (rng (canHomP p))) \/ the carrier of F & b in ( the carrier of (Polynom-Ring p) \ (rng (canHomP p))) \/ the carrier of F ) by B2, XBOOLE_0:def 3;

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

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

.= addemb ((canHomP 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 p) \ (rng (canHomP p))) \/ the carrier of F & b in ( the carrier of (Polynom-Ring p) \ (rng (canHomP p))) \/ the carrier of F ) by B2, XBOOLE_0:def 3;

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

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

.= addemb ((canHomP 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 (canHomP p)) = [: the carrier of (embField (canHomP p)), the carrier of (embField (canHomP 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 (canHomP p)) . x = the multF of F . x

then
the multF of (embField (canHomP p)) = the multF of F
by B;let x be Element of dom the multF of F; :: thesis: the multF of (embField (canHomP 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 p) \ (rng (canHomP p))) \/ the carrier of F & b in ( the carrier of (Polynom-Ring p) \ (rng (canHomP p))) \/ the carrier of F ) by B2, XBOOLE_0:def 3;

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

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

.= multemb ((canHomP 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 p) \ (rng (canHomP p))) \/ the carrier of F & b in ( the carrier of (Polynom-Ring p) \ (rng (canHomP p))) \/ the carrier of F ) by B2, XBOOLE_0:def 3;

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

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

.= multemb ((canHomP 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 (canHomP p) = F by A, C, polyd; :: thesis: verum