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.|

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

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

hence degree p = degree |.p.| ; :: thesis: verum

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;

end;