:: deftheorem defines scalar_prd_prg PRGCOR_2:def 4 :
for b, c being XFinSequence of REAL
for a being Real
for m being Integer holds
( m scalar_prd_prg c,a,b iff ( len c = m & len b = m & ex n being Integer st
( c . 0 = b . 0 & n = b . 0 & ( n <> 0 implies for i being Nat st 1 <= i & i <= n holds
c . i = a * (b . i) ) ) ) );