:: deftheorem Def3 defines inner_prd_prg PRGCOR_2:def 3 :
for a, b being XFinSequence of REAL st b . 0 is Nat & b . 0 < len a holds
for b₃ being Real holds
( b₃ = inner_prd_prg (a,b) iff ex s being XFinSequence of REAL ex n being Integer st
( len s = len a & s . 0 = 0 & n = b . 0 & ( n <> 0 implies for i being Nat st i < n holds
s . (i + 1) = (s . i) + ((a . (i + 1)) * (b . (i + 1))) ) & b₃ = s . n ) );