let k, n be Nat; :: thesis: for L being non empty right_complementable add-associative right_zeroed distributive doubleLoopStr
for a being Polynomial of L holds (n * a) . k = n * (a . k)
let L be non empty right_complementable add-associative right_zeroed distributive doubleLoopStr ; :: thesis: for a being Polynomial of L holds (n * a) . k = n * (a . k)
let a be Polynomial of L; :: thesis: (n * a) . k = n * (a . k)
set PRR = Polynom-Ring L;
defpred S1[ Nat] means ($1 * a) . k = $1 * (a . k);
0 * a = 0. (Polynom-Ring L) by BINOM:12
.= 0_. L by POLYNOM3:def 10 ;
then (0 * a) . k = 0. L by ORDINAL1:def 12, FUNCOP_1:7
.= 0 * (a . k) by BINOM:12 ;
then A1: S1[ 0 ] ;
A2: for i being Nat st S1[i] holds
S1[i + 1]
proof
let i be Nat; :: thesis: ( S1[i] implies S1[i + 1] )
assume A3: S1[i] ; :: thesis: S1[i + 1]
(i + 1) * a = (@ a) + (i * (@ a)) by BINOM:def 3
.= a + (i * a) by POLYNOM3:def 10 ;
hence ((i + 1) * a) . k = (a . k) + ((i * a) . k) by NORMSP_1:def 2
.= (i + 1) * (a . k) by A3, BINOM:def 3 ;
:: thesis: verum
end;
for i being Nat holds S1[i] from NAT_1:sch 2(A1, A2);
 hence (n * a) . k = n * (a . k) ; :: thesis: verum