let L be non empty right_complementable almost_left_invertible add-associative right_zeroed well-unital distributive associative commutative doubleLoopStr ; :: thesis: for p being Polynomial of L
for v being Element of L st v <> 0. L holds
len (v * p) = len p
let p be Polynomial of L; :: thesis: for v being Element of L st v <> 0. L holds
len (v * p) = len p
let v be Element of L; :: thesis: ( v <> 0. L implies len (v * p) = len p )
assume A1: v <> 0. 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 Def4;
hence p . i = 0. L by A1, VECTSP_1:12; :: 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 Def4
.= 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