reconsider q0 = <%(In (0,REAL))%> as XFinSequence of REAL ; set n2 = len a; reconsider nn2 = b .0 as NatbyA1; reconsider nn = nn2 as Integer ; defpred S1[ Nat] means ex q being XFinSequence of REAL st ( len q = $1 + 1 & q .0=0 & ( for k being Nat st k < $1 & k < nn2 holds q .(k + 1)=(q . k)+((a .(k + 1))*(b .(k + 1))) ) ); A3:
for k being Nat st k <0 & k < nn2 holds q0 .(k + 1)=(q0 . k)+((a .(k + 1))*(b .(k + 1)))
; A4:
for k being Nat st S1[k] holds S1[k + 1]