let F be Field; :: thesis: for p being non zero Polynomial of F
for E1, E2 being FieldExtension of F
for i being Function of E1,E2 st i is F -fixing & i is isomorphism holds
for a being Element of E1 holds multiplicity (p,a) = multiplicity (p,(i . a))
let p be non zero Polynomial of F; :: thesis: for E1, E2 being FieldExtension of F
for i being Function of E1,E2 st i is F -fixing & i is isomorphism holds
for a being Element of E1 holds multiplicity (p,a) = multiplicity (p,(i . a))
let E1, E2 be FieldExtension of F; :: thesis: for i being Function of E1,E2 st i is F -fixing & i is isomorphism holds
for a being Element of E1 holds multiplicity (p,a) = multiplicity (p,(i . a))
let i be Function of E1,E2; :: thesis: ( i is F -fixing & i is isomorphism implies for a being Element of E1 holds multiplicity (p,a) = multiplicity (p,(i . a)) )
assume AS: ( i is F -fixing & i is isomorphism ) ; :: thesis: for a being Element of E1 holds multiplicity (p,a) = multiplicity (p,(i . a))
let a be Element of E1; :: thesis: multiplicity (p,a) = multiplicity (p,(i . a))
set n = multiplicity (p,a);
reconsider E2 = E2 as E1 -isomorphic FieldExtension of F by AS, RING_3:def 4;
reconsider i = i as Isomorphism of E1,E2 by AS;
p is Polynomial of E1 by FIELD_4:8;
then reconsider q = p as Element of the carrier of (Polynom-Ring E1) by POLYNOM3:def 10;
p <> 0_. F ;
then p <> 0_. E1 by FIELD_4:12;
then reconsider q = q as non zero Element of the carrier of (Polynom-Ring E1) by UPROOTS:def 5;
reconsider E3 = E2 as E1 -homomorphic Field ;
reconsider h = i as additive Function of E1,E3 ;

H: now :: thesis: not (PolyHom h) . q = 0_. E2

assume I1: (PolyHom h) . q = 0_. E2 ; :: thesis: contradiction
I2: (PolyHom h) . (0_. E1) = 0_. E2 by FIELD_1:22;
0_. E1 in the carrier of (Polynom-Ring E1) by POLYNOM3:def 10;
hence contradiction by I1, I2, FUNCT_2:19; :: thesis: verum

end;

then reconsider iq = (PolyHom h) . q as non zero Polynomial of E2 by UPROOTS:def 5;
reconsider r = q as non zero Element of the carrier of (Polynom-Ring E1) ;
reconsider hr = (PolyHom h) . r as Polynomial of E3 ;
reconsider hr = hr as non zero Polynomial of E3 by H, UPROOTS:def 5;
reconsider Xan = (X- a) `^ (multiplicity (p,a)) as Element of the carrier of (Polynom-Ring E1) by POLYNOM3:def 10;
reconsider Xan1 = (X- a) `^ ((multiplicity (p,a)) + 1) as Element of the carrier of (Polynom-Ring E1) by POLYNOM3:def 10;
H: multiplicity (p,a) = multiplicity (q,a) by FIELD_14:def 6;
then A: ( (X- a) `^ (multiplicity (p,a)) divides q & not (X- a) `^ ((multiplicity (p,a)) + 1) divides q ) by FIELD_14:67;
B: (PolyHom h) . Xan divides (PolyHom h) . r by H, FIELD_12:3, FIELD_14:67;

C: now :: thesis: not (PolyHom h) . Xan1 divides (PolyHom h) . r

assume C1: (PolyHom h) . Xan1 divides (PolyHom h) . r ; :: thesis: contradiction
reconsider E1 = E1 as E2 -isomorphic FieldExtension of F by RING_3:74;
reconsider k = i " as Isomorphism of E2,E1 by RING_3:73;
reconsider E4 = E1 as E2 -homomorphic E2 -monomorphic Field ;
reconsider j = k as Monomorphism of E2,E4 ;
reconsider iXan = (PolyHom h) . Xan1, ir = (PolyHom h) . r as Element of the carrier of (Polynom-Ring E2) ;
C3: (PolyHom j) . ((PolyHom h) . Xan1) = Xan1

proof

reconsider u = (PolyHom j) . iXan as Polynomial of E1 ;

now :: thesis: for o being object st o in NAT holds
u . o = Xan1 . o

let o be object ; :: thesis: ( o in NAT implies u . o = Xan1 . o )
assume o in NAT ; :: thesis: u . o = Xan1 . o
then reconsider m = o as Nat ;
C4: dom h = the carrier of E1 by FUNCT_2:def 1;
u . m = j . (iXan . m) by FIELD_1:def 2
.= j . (h . (Xan1 . m)) by FIELD_1:def 2
.= Xan1 . m by C4, FUNCT_1:34 ;
hence u . o = Xan1 . o ; :: thesis: verum

end;

hence (PolyHom j) . ((PolyHom h) . Xan1) = Xan1 by FUNCT_2:12; :: thesis: verum

end;

(PolyHom j) . ((PolyHom h) . r) = r

proof

reconsider u = (PolyHom j) . ir as Polynomial of E1 ;

now :: thesis: for o being object st o in NAT holds
u . o = r . o

let o be object ; :: thesis: ( o in NAT implies u . o = r . o )
assume o in NAT ; :: thesis: u . o = r . o
then reconsider m = o as Nat ;
C4: dom h = the carrier of E1 by FUNCT_2:def 1;
u . m = j . (ir . m) by FIELD_1:def 2
.= j . (h . (r . m)) by FIELD_1:def 2
.= r . m by C4, FUNCT_1:34 ;
hence u . o = r . o ; :: thesis: verum

end;

hence (PolyHom j) . ((PolyHom h) . r) = r by FUNCT_2:12; :: thesis: verum

end;

hence contradiction by C3, C1, FIELD_12:3, A; :: thesis: verum

end;

( (PolyHom h) . Xan = (X- (h . a)) `^ (multiplicity (p,a)) & (PolyHom h) . Xan1 = (X- (h . a)) `^ ((multiplicity (p,a)) + 1) ) by aXn;
then D: multiplicity (hr,(h . a)) = multiplicity (p,a) by B, C, FIELD_14:67;
(PolyHom h) . p = p

proof

reconsider u = (PolyHom h) . q as Polynomial of E3 ;

now :: thesis: for o being object st o in rng u holds
o in the carrier of F

let o be object ; :: thesis: ( o in rng u implies o in the carrier of F )
assume o in rng u ; :: thesis: o in the carrier of F
then consider v being object such that
E: ( v in dom u & u . v = o ) by FUNCT_1:def 3;
dom u = NAT by FUNCT_2:def 1;
then reconsider v = v as Nat by E;
u . v = h . (p . v) by FIELD_1:def 2
.= p . v by AS ;
hence o in the carrier of F by E; :: thesis: verum

end;

then rng u c= the carrier of F ;
then E: (PolyHom h) . p is Function of NAT, the carrier of F by FUNCT_2:6;

now :: thesis: for o being object st o in NAT holds
u . o = p . o

let o be object ; :: thesis: ( o in NAT implies u . o = p . o )
assume o in NAT ; :: thesis: u . o = p . o
then reconsider m = o as Nat ;
u . m = h . (p . m) by FIELD_1:def 2
.= p . m by AS ;
hence u . o = p . o ; :: thesis: verum

end;

hence (PolyHom h) . p = p by E, FUNCT_2:12; :: thesis: verum

end;

hence multiplicity (p,a) = multiplicity (p,(i . a)) by D, FIELD_14:def 6; :: thesis: verum