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 S_{1}[ 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: S_{1}[ 0 ]
;

A2: for i being Nat st S_{1}[i] holds

S_{1}[i + 1]
_{1}[i]
from NAT_1:sch 2(A1, A2);

hence (n * a) . k = n * (a . k) ; :: thesis: verum

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 S

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: S

A2: for i being Nat st S

S

proof

for i being Nat holds S
let i be Nat; :: thesis: ( S_{1}[i] implies S_{1}[i + 1] )

assume A3: S_{1}[i]
; :: thesis: S_{1}[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;assume A3: S

(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

hence (n * a) . k = n * (a . k) ; :: thesis: verum