let n be Ordinal; :: thesis: for p being Polynomial of n,F_Real holds degree p = degree |.p.|

let p be Polynomial of n,F_Real; :: thesis: degree p = degree |.p.|

let p be Polynomial of n,F_Real; :: thesis: degree p = degree |.p.|

per cases
( p = 0_ (n,F_Real) or p <> 0_ (n,F_Real) )
;

end;

suppose A1:
p <> 0_ (n,F_Real)
; :: thesis: degree p = degree |.p.|

then consider s being bag of n such that

A2: ( s in Support p & degree p = degree s ) by Def3;

A3: |.p.| <> 0_ (n,F_Real) by A1, Th7;

then consider sM being bag of n such that

A4: ( sM in Support |.p.| & degree |.p.| = degree sM ) by Def3;

Support |.p.| = Support p by Th3;

then ( degree p <= degree |.p.| & degree |.p.| <= degree p ) by A2, A1, Def3, A4, A3;

hence degree p = degree |.p.| by XXREAL_0:1; :: thesis: verum

end;A2: ( s in Support p & degree p = degree s ) by Def3;

A3: |.p.| <> 0_ (n,F_Real) by A1, Th7;

then consider sM being bag of n such that

A4: ( sM in Support |.p.| & degree |.p.| = degree sM ) by Def3;

Support |.p.| = Support p by Th3;

then ( degree p <= degree |.p.| & degree |.p.| <= degree p ) by A2, A1, Def3, A4, A3;

hence degree p = degree |.p.| by XXREAL_0:1; :: thesis: verum