let n be Nat; :: thesis: for L being non empty ZeroStr
for z being Element of L st z <> 0. L holds
for p being Polynomial of L st p = (0_. L) +* (n,z) holds
len p = n + 1
let L be non empty ZeroStr ; :: thesis: for z being Element of L st z <> 0. L holds
for p being Polynomial of L st p = (0_. L) +* (n,z) holds
len p = n + 1
let z be Element of L; :: thesis: ( z <> 0. L implies for p being Polynomial of L st p = (0_. L) +* (n,z) holds
len p = n + 1 )
assume A1: z <> 0. L ; :: thesis: for p being Polynomial of L st p = (0_. L) +* (n,z) holds
len p = n + 1
let p be Polynomial of L; :: thesis: ( p = (0_. L) +* (n,z) implies len p = n + 1 )
assume A2: p = (0_. L) +* (n,z) ; :: thesis: len p = n + 1
A3: n + 1 is_at_least_length_of p

proof

let i be Nat; :: according to ALGSEQ_1:def 2 :: thesis: ( not n + 1 <= i or p . i = 0. L )
assume A4: i >= n + 1 ; :: thesis: p . i = 0. L
i > n by A4, NAT_1:13;
hence p . i = (0_. L) . i by A2, FUNCT_7:32
.= 0. L by ORDINAL1:def 12, FUNCOP_1:7 ;
:: thesis: verum

end;

for m being Nat st m is_at_least_length_of p holds
n + 1 <= m

proof

let m be Nat; :: thesis: ( m is_at_least_length_of p implies n + 1 <= m )
assume A5: m is_at_least_length_of p ; :: thesis: n + 1 <= m
assume A6: n + 1 > m ; :: thesis: contradiction
dom (0_. L) = NAT by FUNCOP_1:13;
then p . n = z by A2, ORDINAL1:def 12, FUNCT_7:31;
hence contradiction by A1, A5, A6, NAT_1:13; :: thesis: verum

end;

hence len p = n + 1 by A3, ALGSEQ_1:def 3; :: thesis: verum