let L be non empty ZeroStr ; :: thesis: for p being Polynomial of L
for n being Element of NAT holds
( n >= len p iff n is_at_least_length_of p )
let p be Polynomial of L; :: thesis: for n being Element of NAT holds
( n >= len p iff n is_at_least_length_of p )
let n be Element of NAT ; :: thesis: ( n >= len p iff n is_at_least_length_of p )
thus ( n >= len p implies n is_at_least_length_of p ) :: thesis: ( n is_at_least_length_of p implies n >= len p )

proof

assume A1: n >= len p ; :: thesis: n is_at_least_length_of p
let i be Nat; :: according to ALGSEQ_1:def 2 :: thesis: ( not n <= i or p . i = 0. L )
assume i >= n ; :: thesis: p . i = 0. L
hence p . i = 0. L by A1, ALGSEQ_1:8, XXREAL_0:2; :: thesis: verum

end;

assume n is_at_least_length_of p ; :: thesis: n >= len p
hence n >= len p by ALGSEQ_1:def 3; :: thesis: verum