let R be Ring; :: thesis: for a, b, x being Element of R holds x * <%b,a%> = <%(x * b),(x * a)%>
let a, b, x be Element of R; :: thesis: x * <%b,a%> = <%(x * b),(x * a)%>
set p = <%(x * b),(x * a)%>;
H: ( len <%b,a%> <= 2 & len <%(x * b),(x * a)%> <= 2 ) by POLYNOM5:39;

now :: thesis: for i being Element of NAT holds (x * <%b,a%>) . i = <%(x * b),(x * a)%> . i

let i be Element of NAT ; :: thesis: (x * <%b,a%>) . b₁ = <%(x * b),(x * a)%> . b₁
( i <= 1 implies not not i = 0 & ... & not i = 1 ) ;

per cases then ( i = 0 or i = 1 or i > 1 ) ;

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

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

end;

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

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

end;

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

then i + 1 > 1 + 1 by XREAL_1:6;
then C: i >= 2 by NAT_1:13;
then <%b,a%> . i = 0. R by H, XXREAL_0:2, ALGSEQ_1:8;
hence (x * <%b,a%>) . i = x * (0. R) by POLYNOM5:def 4
.= <%(x * b),(x * a)%> . i by C, H, XXREAL_0:2, ALGSEQ_1:8 ;
:: thesis: verum

end;

end;

end;

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