let L be domRing; :: thesis: for p being Polynomial of L
for a being non zero Element of L holds len (a * p) = len p
let p be Polynomial of L; :: thesis: for a being non zero Element of L holds len (a * p) = len p
let v be non zero Element of L; :: thesis: len (v * p) = len p

A2: now :: thesis: for n being Nat st n is_at_least_length_of v * p holds
len p <= n

let n be Nat; :: thesis: ( n is_at_least_length_of v * p implies len p <= n )
assume A3: n is_at_least_length_of v * p ; :: thesis: len p <= n
n is_at_least_length_of p

proof

let i be Nat; :: according to ALGSEQ_1:def 2 :: thesis: ( not n <= i or p . i = 0. L )
reconsider i1 = i as Element of NAT by ORDINAL1:def 12;
assume i >= n ; :: thesis: p . i = 0. L
then (v * p) . i = 0. L by A3;
then v * (p . i1) = 0. L by POLYNOM5:def 4;
hence p . i = 0. L by VECTSP_2:def 1; :: thesis: verum

end;

hence len p <= n by ALGSEQ_1:def 3; :: thesis: verum

end;

len p is_at_least_length_of v * p

proof

let i be Nat; :: according to ALGSEQ_1:def 2 :: thesis: ( not len p <= i or (v * p) . i = 0. L )
assume A4: i >= len p ; :: thesis: (v * p) . i = 0. L
reconsider ii = i as Element of NAT by ORDINAL1:def 12;
thus (v * p) . i = v * (p . ii) by POLYNOM5:def 4
.= v * (0. L) by A4, ALGSEQ_1:8
.= 0. L ; :: thesis: verum

end;

hence len (v * p) = len p by A2, ALGSEQ_1:def 3; :: thesis: verum