let R be Ring; for a, b, c, x being Element of R holds x * <%c,b,a%> = <%(x * c),(x * b),(x * a)%>
let a, b, c, x be Element of R; x * <%c,b,a%> = <%(x * c),(x * b),(x * a)%>
set p = <%(x * c),(x * b),(x * a)%>;
H:
( len <%c,b,a%> <= 3 & len <%(x * c),(x * b),(x * a)%> <= 3 )
by qua2;
now for i being Element of NAT holds (x * <%c,b,a%>) . i = <%(x * c),(x * b),(x * a)%> . ilet i be
Element of
NAT ;
(x * <%c,b,a%>) . b1 = <%(x * c),(x * b),(x * a)%> . b1
(
i <= 2 implies not not
i = 0 & ... & not
i = 2 )
;
per cases then
( i = 0 or i = 1 or i = 2 or i > 2 )
;
suppose
i > 2
;
(x * <%c,b,a%>) . b1 = <%(x * c),(x * b),(x * a)%> . b1then
i + 1
> 2
+ 1
by XREAL_1:6;
then C:
i >= 3
by NAT_1:13;
then
<%c,b,a%> . i = 0. R
by H, XXREAL_0:2, ALGSEQ_1:8;
hence (x * <%c,b,a%>) . i =
x * (0. R)
by POLYNOM5:def 4
.=
<%(x * c),(x * b),(x * a)%> . i
by C, H, XXREAL_0:2, ALGSEQ_1:8
;
verum end; end; end;
hence
x * <%c,b,a%> = <%(x * c),(x * b),(x * a)%>
; verum