reconsider nn2 = b . 0 as Nat by A1;
reconsider nn = nn2 as Integer ;
set n2 = len a;
defpred S₁[ natural number ] means ex q being XFinSequence of 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))) ) );
reconsider q0 = <%0 %> as XFinSequence of ;
A2: ( len q0 = 1 & q0 . 0 = 0 ) by AFINSQ_1:def 5;
for k being Nat st k < 0 & k < nn2 holds
q0 . (k + 1) = (q0 . k) + ((a . (k + 1)) * (b . (k + 1))) ;
then A3: S₁[ 0 ] by A2;
A4: for k being natural number st S₁[k] holds
S₁[k + 1]

proof

let k be natural number ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume S₁[k] ; :: thesis: S₁[k + 1]
then consider q2 being XFinSequence of such that
A5: ( len q2 = k + 1 & q2 . 0 = 0 & ( for k2 being Nat st k2 < k & k2 < nn2 holds
q2 . (k2 + 1) = (q2 . k2) + ((a . (k2 + 1)) * (b . (k2 + 1))) ) ) ;
reconsider k0 = k as Nat ;
reconsider q3 = q2 ^ <%((q2 . k0) + ((a . (k0 + 1)) * (b . (k0 + 1))))%> as XFinSequence of ;
A6: len q3 = (len q2) + (len <%((q2 . k0) + ((a . (k0 + 1)) * (b . (k0 + 1))))%>) by AFINSQ_1:20
.= (k + 1) + 1 by A5, AFINSQ_1:36 ;
0 in len q2 by A5, NAT_1:45;
then A7: q3 . 0 = 0 by A5, AFINSQ_1:def 4;
for k2 being Nat st k2 < k + 1 & k2 < nn2 holds
q3 . (k2 + 1) = (q3 . k2) + ((a . (k2 + 1)) * (b . (k2 + 1)))

proof

let k2 be Nat; :: thesis: ( k2 < k + 1 & k2 < nn2 implies q3 . (k2 + 1) = (q3 . k2) + ((a . (k2 + 1)) * (b . (k2 + 1))) )
assume A8: ( k2 < k + 1 & k2 < nn2 ) ; :: thesis: q3 . (k2 + 1) = (q3 . k2) + ((a . (k2 + 1)) * (b . (k2 + 1)))
then A9: k2 <= k by NAT_1:13;

now

per cases ( k2 < k or k2 = k ) by A9, XXREAL_0:1;

case A10: k2 < k ; :: thesis: q3 . (k2 + 1) = (q3 . k2) + ((a . (k2 + 1)) * (b . (k2 + 1)))

then k2 + 1 < k + 1 by XREAL_1:8;
then k2 + 1 in len q2 by A5, NAT_1:45;
then A11: q3 . (k2 + 1) = q2 . (k2 + 1) by AFINSQ_1:def 4;
k2 < len q2 by A5, A10, NAT_1:13;
then k2 in dom q2 by NAT_1:45;
then q3 . k2 = q2 . k2 by AFINSQ_1:def 4;
hence q3 . (k2 + 1) = (q3 . k2) + ((a . (k2 + 1)) * (b . (k2 + 1))) by A5, A8, A10, A11; :: thesis: verum

end;

case A12: k2 = k ; :: thesis: q3 . (k2 + 1) = (q3 . k2) + ((a . (k2 + 1)) * (b . (k2 + 1)))

A13: <%((q2 . k0) + ((a . (k0 + 1)) * (b . (k0 + 1))))%> . 0 = (q2 . k0) + ((a . (k0 + 1)) * (b . (k0 + 1))) by AFINSQ_1:38;
k2 < k2 + 1 by NAT_1:13;
then A14: k2 in dom q2 by A5, A12, NAT_1:45;
0 in 1 by NAT_1:45;
then 0 in dom <%((q2 . k0) + ((a . (k0 + 1)) * (b . (k0 + 1))))%> by AFINSQ_1:def 5;
then q3 . ((k2 + 1) + 0 ) = (q2 . k0) + ((a . (k0 + 1)) * (b . (k0 + 1))) by A5, A12, A13, AFINSQ_1:def 4;
hence q3 . (k2 + 1) = (q3 . k2) + ((a . (k2 + 1)) * (b . (k2 + 1))) by A12, A14, AFINSQ_1:def 4; :: thesis: verum

end;

end;

end;

hence q3 . (k2 + 1) = (q3 . k2) + ((a . (k2 + 1)) * (b . (k2 + 1))) ; :: thesis: verum

end;

hence S₁[k + 1] by A6, A7; :: thesis: verum

end;

for k being natural number holds S₁[k] from NAT_1:sch 2(A3, A4);
then consider q being XFinSequence of such that
A15: ( len q = ((len a) -' 1) + 1 & q . 0 = 0 & ( for k3 being Nat st k3 < (len a) -' 1 & k3 < nn2 holds
q . (k3 + 1) = (q . k3) + ((a . (k3 + 1)) * (b . (k3 + 1))) ) ) ;
len a >= 0 + 1 by A1, NAT_1:13;
then (len a) - 1 >= 0 by XREAL_1:50;
then A16: (len a) -' 1 = (len a) - 1 by XREAL_0:def 2;
A17: ( nn <> 0 implies for i being Nat st i < nn holds
q . (i + 1) = (q . i) + ((a . (i + 1)) * (b . (i + 1))) )

proof

assume nn <> 0 ; :: thesis: for i being Nat st i < nn holds
q . (i + 1) = (q . i) + ((a . (i + 1)) * (b . (i + 1)))
thus for i being Nat st i < nn holds
q . (i + 1) = (q . i) + ((a . (i + 1)) * (b . (i + 1))) :: thesis: verum

proof

let i be Nat; :: thesis: ( i < nn implies q . (i + 1) = (q . i) + ((a . (i + 1)) * (b . (i + 1))) )
assume A18: i < nn ; :: thesis: q . (i + 1) = (q . i) + ((a . (i + 1)) * (b . (i + 1)))
nn + 1 <= len a by A1, NAT_1:13;
then (nn + 1) - 1 <= (len a) - 1 by XREAL_1:11;
then i < (len a) -' 1 by A16, A18, XXREAL_0:2;
hence q . (i + 1) = (q . i) + ((a . (i + 1)) * (b . (i + 1))) by A15, A18; :: thesis: verum

end;

end;

reconsider ss2 = q . nn2 as Real ;
ex s being XFinSequence of 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))) ) & ss2 = s . n ) by A15, A16, A17;
hence ex b₁ being Real ex s being XFinSequence of 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 ) ; :: thesis: verum