let c, c1 be non empty positive-yielding XFinSequence of REAL ; :: thesis: for a being Real st c1 = a (#) c holds
for x being Nat holds (polynom c1) . x = a * ((polynom c) . x)
let a be Real; :: thesis: ( c1 = a (#) c implies for x being Nat holds (polynom c1) . x = a * ((polynom c) . x) )
assume AS: c1 = a (#) c ; :: thesis: for x being Nat holds (polynom c1) . x = a * ((polynom c) . x)
let x be Nat; :: thesis: (polynom c1) . x = a * ((polynom c) . x)
D1: dom (c1 (#) (seq_a^ (x,1,0))) = dom c1 by ASYMPT_2:26
.= dom c by VALUED_1:def 5, AS ;
D2: dom (a (#) (c (#) (seq_a^ (x,1,0)))) = dom (c (#) (seq_a^ (x,1,0))) by VALUED_1:def 5
.= dom c by ASYMPT_2:26 ;
for i being object st i in dom (c1 (#) (seq_a^ (x,1,0))) holds
(c1 (#) (seq_a^ (x,1,0))) . i = (a (#) (c (#) (seq_a^ (x,1,0)))) . i

proof

let i be object ; :: thesis: ( i in dom (c1 (#) (seq_a^ (x,1,0))) implies (c1 (#) (seq_a^ (x,1,0))) . i = (a (#) (c (#) (seq_a^ (x,1,0)))) . i )
assume D3: i in dom (c1 (#) (seq_a^ (x,1,0))) ; :: thesis: (c1 (#) (seq_a^ (x,1,0))) . i = (a (#) (c (#) (seq_a^ (x,1,0)))) . i
then D4: i in dom c1 by ASYMPT_2:26;
thus (c1 (#) (seq_a^ (x,1,0))) . i = (c1 . i) * ((seq_a^ (x,1,0)) . i) by D4, ASYMPT_2:26
.= (a * (c . i)) * ((seq_a^ (x,1,0)) . i) by AS, VALUED_1:6
.= a * ((c . i) * ((seq_a^ (x,1,0)) . i))
.= a * ((c (#) (seq_a^ (x,1,0))) . i) by D3, D1, ASYMPT_2:26
.= (a (#) (c (#) (seq_a^ (x,1,0)))) . i by VALUED_1:6 ; :: thesis: verum

end;

then P2: c1 (#) (seq_a^ (x,1,0)) = a (#) (c (#) (seq_a^ (x,1,0))) by D1, D2;
thus (polynom c1) . x = Sum (c1 (#) (seq_a^ (x,1,0))) by ASYMPT_2:def 2
.= a * (Sum (c (#) (seq_a^ (x,1,0)))) by AFINSQ_2:64, P2
.= a * ((polynom c) . x) by ASYMPT_2:def 2 ; :: thesis: verum