let n be Nat; :: thesis: for L being non empty ZeroStr
for p being Polynomial of L st n > (len p) -' 1 holds
p || n = p
let L be non empty ZeroStr ; :: thesis: for p being Polynomial of L st n > (len p) -' 1 holds
p || n = p
let p be Polynomial of L; :: thesis: ( n > (len p) -' 1 implies p || n = p )
assume A1: n > (len p) -' 1 ; :: thesis: p || n = p
let m be Element of NAT ; :: according to FUNCT_2:def 8 :: thesis: (p || n) . m = p . m
per cases ( p = 0_. L or ( m = n & p <> 0_. L ) or m <> n ) ;
suppose p = 0_. L ; :: thesis: (p || n) . m = p . m
hence (p || n) . m = p . m ; :: thesis: verum
end;
suppose that A2: m = n and
A3: p <> 0_. L ; :: thesis: (p || n) . m = p . m
0 <> len p by A3, POLYNOM4:5;
then 0 - 1 < (len p) - 1 by XREAL_1:14;
then (- 1) + 1 <= (len p) - 1 by INT_1:7;
then ((len p) -' 1) + 1 = len p by NAT_D:72;
then n >= len p by A1, NAT_1:13;
hence p . m = 0. L by A2, ALGSEQ_1:8
.= (p || n) . m by A2, Th32 ;
:: thesis: verum
end;
suppose m <> n ; :: thesis: (p || n) . m = p . m
hence (p || n) . m = p . m by FUNCT_7:32; :: thesis: verum
end;
end;