let n be Ordinal; :: thesis: for p being Polynomial of n,F_Real st |.p.| = 0_ (n,F_Real) holds
p = 0_ (n,F_Real)
let p be Polynomial of n,F_Real; :: thesis: ( |.p.| = 0_ (n,F_Real) implies p = 0_ (n,F_Real) )
assume A1: |.p.| = 0_ (n,F_Real) ; :: thesis: p = 0_ (n,F_Real)

now :: thesis: for b being Element of Bags n holds p . b = (0_ (n,F_Real)) . b

let b be Element of Bags n; :: thesis: p . b = (0_ (n,F_Real)) . b
|.(p . b).| = |.p.| . b by Def1
.= 0 by A1 ;
hence p . b = (0_ (n,F_Real)) . b ; :: thesis: verum

end;

hence p = 0_ (n,F_Real) ; :: thesis: verum