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

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

len p is_at_least_length_of v * p
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

end;assume A3: n is_at_least_length_of v * p ; :: thesis: len p <= n

n is_at_least_length_of p

proof

hence
len p <= n
by ALGSEQ_1:def 3; :: thesis: verum
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;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

proof

hence
len (v * p) = len p
by A2, ALGSEQ_1:def 3; :: thesis: verum
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;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