let R be Ring; :: thesis: 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; :: thesis: 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 :: thesis: for i being Element of NAT holds (x * <%c,b,a%>) . i = <%(x * c),(x * b),(x * a)%> . i

let i be Element of NAT ; :: thesis: (x * <%c,b,a%>) . b₁ = <%(x * c),(x * b),(x * a)%> . b₁
( 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 B: i = 0 ; :: thesis: (x * <%c,b,a%>) . b₁ = <%(x * c),(x * b),(x * a)%> . b₁

then <%c,b,a%> . i = c by qua1;
hence (x * <%c,b,a%>) . i = x * c by POLYNOM5:def 4
.= <%(x * c),(x * b),(x * a)%> . i by B, qua1 ;
:: thesis: verum

end;

suppose B: i = 1 ; :: thesis: (x * <%c,b,a%>) . b₁ = <%(x * c),(x * b),(x * a)%> . b₁

then <%c,b,a%> . i = b by qua1;
hence (x * <%c,b,a%>) . i = x * b by POLYNOM5:def 4
.= <%(x * c),(x * b),(x * a)%> . i by B, qua1 ;
:: thesis: verum

end;

suppose B: i = 2 ; :: thesis: (x * <%c,b,a%>) . b₁ = <%(x * c),(x * b),(x * a)%> . b₁

then <%c,b,a%> . i = a by qua1;
hence (x * <%c,b,a%>) . i = x * a by POLYNOM5:def 4
.= <%(x * c),(x * b),(x * a)%> . i by B, qua1 ;
:: thesis: verum

end;

suppose i > 2 ; :: thesis: (x * <%c,b,a%>) . b₁ = <%(x * c),(x * b),(x * a)%> . b₁

then 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 ;
:: thesis: verum

end;

end;

end;

hence x * <%c,b,a%> = <%(x * c),(x * b),(x * a)%> ; :: thesis: verum