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₁[ 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₁[ 0 ] ;
A2: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A3: S₁[i] ; :: thesis: S₁[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 S₁[i] from NAT_1:sch 2(A1, A2);
hence (~ (n * (@ a))) . k = n * (a . k) ; :: thesis: verum