reconsider q0 = <%(In (0,REAL))%> as XFinSequence of REAL ;
set n2 = len a;
reconsider nn2 = b . 0 as Nat by A1;
reconsider nn = nn2 as Integer ;
defpred S₁[ 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 S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
reconsider k0 = k as Nat ;
assume S₁[k] ; :: thesis: S₁[k + 1]
then consider q2 being XFinSequence of REAL such that
A5: len q2 = k + 1 and
A6: q2 . 0 = 0 and
A7: for k2 being Nat st k2 < k & k2 < nn2 holds
q2 . (k2 + 1) = (q2 . k2) + ((a . (k2 + 1)) * (b . (k2 + 1))) ;
reconsider qab = (q2 . k0) + ((a . (k0 + 1)) * (b . (k0 + 1))) as Element of REAL by XREAL_0:def 1;
set q3 = q2 ^ <%qab%>;
0 in len q2 by A5, AFINSQ_1:86;
then A8: (q2 ^ <%qab%>) . 0 = 0 by A6, AFINSQ_1:def 3;
A9: for k2 being Nat st k2 < k + 1 & k2 < nn2 holds
(q2 ^ <%qab%>) . (k2 + 1) = ((q2 ^ <%qab%>) . k2) + ((a . (k2 + 1)) * (b . (k2 + 1)))

proof

let k2 be Nat; :: thesis: ( k2 < k + 1 & k2 < nn2 implies (q2 ^ <%qab%>) . (k2 + 1) = ((q2 ^ <%qab%>) . k2) + ((a . (k2 + 1)) * (b . (k2 + 1))) )
assume that
A10: k2 < k + 1 and
A11: k2 < nn2 ; :: thesis: (q2 ^ <%qab%>) . (k2 + 1) = ((q2 ^ <%qab%>) . k2) + ((a . (k2 + 1)) * (b . (k2 + 1)))
A12: k2 <= k by A10, NAT_1:13;

now :: thesis: ( ( k2 < k & (q2 ^ <%qab%>) . (k2 + 1) = ((q2 ^ <%qab%>) . k2) + ((a . (k2 + 1)) * (b . (k2 + 1))) ) or ( k2 = k & (q2 ^ <%qab%>) . (k2 + 1) = ((q2 ^ <%qab%>) . k2) + ((a . (k2 + 1)) * (b . (k2 + 1))) ) )

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

case A13: k2 < k ; :: thesis: (q2 ^ <%qab%>) . (k2 + 1) = ((q2 ^ <%qab%>) . k2) + ((a . (k2 + 1)) * (b . (k2 + 1)))

then k2 < len q2 by A5, NAT_1:13;
then k2 in dom q2 by AFINSQ_1:86;
then A14: (q2 ^ <%qab%>) . k2 = q2 . k2 by AFINSQ_1:def 3;
k2 + 1 < k + 1 by A13, XREAL_1:6;
then k2 + 1 in len q2 by A5, AFINSQ_1:86;
then (q2 ^ <%qab%>) . (k2 + 1) = q2 . (k2 + 1) by AFINSQ_1:def 3;
hence (q2 ^ <%qab%>) . (k2 + 1) = ((q2 ^ <%qab%>) . k2) + ((a . (k2 + 1)) * (b . (k2 + 1))) by A7, A11, A13, A14; :: thesis: verum

end;

case A15: k2 = k ; :: thesis: (q2 ^ <%qab%>) . (k2 + 1) = ((q2 ^ <%qab%>) . k2) + ((a . (k2 + 1)) * (b . (k2 + 1)))

0 in Segm 1 by NAT_1:44;
then ( <%((q2 . k0) + ((a . (k0 + 1)) * (b . (k0 + 1))))%> . 0 = (q2 . k0) + ((a . (k0 + 1)) * (b . (k0 + 1))) & 0 in dom <%((q2 . k0) + ((a . (k0 + 1)) * (b . (k0 + 1))))%> ) by AFINSQ_1:def 4;
then A16: (q2 ^ <%qab%>) . ((k2 + 1) + 0) = (q2 . k0) + ((a . (k0 + 1)) * (b . (k0 + 1))) by A5, A15, AFINSQ_1:def 3;
k2 < k2 + 1 by NAT_1:13;
then k2 in dom q2 by A5, A15, AFINSQ_1:86;
hence (q2 ^ <%qab%>) . (k2 + 1) = ((q2 ^ <%qab%>) . k2) + ((a . (k2 + 1)) * (b . (k2 + 1))) by A15, A16, AFINSQ_1:def 3; :: thesis: verum

end;

end;

end;

hence (q2 ^ <%qab%>) . (k2 + 1) = ((q2 ^ <%qab%>) . k2) + ((a . (k2 + 1)) * (b . (k2 + 1))) ; :: thesis: verum

end;

len (q2 ^ <%qab%>) = (len q2) + (len <%((q2 . k0) + ((a . (k0 + 1)) * (b . (k0 + 1))))%>) by AFINSQ_1:17
.= (k + 1) + 1 by A5, AFINSQ_1:33 ;
hence S₁[k + 1] by A8, A9; :: thesis: verum

end;

( len q0 = 1 & q0 . 0 = In (0,REAL) ) by AFINSQ_1:def 4;
then A17: S₁[ 0 ] by A3;
for k being Nat holds S₁[k] from NAT_1:sch 2(A17, A4);
then consider q being XFinSequence of REAL such that
A18: ( len q = ((len a) -' 1) + 1 & q . 0 = 0 ) and
A19: for k3 being Nat st k3 < (len a) -' 1 & k3 < nn2 holds
q . (k3 + 1) = (q . k3) + ((a . (k3 + 1)) * (b . (k3 + 1))) ;
reconsider ss2 = q . nn2 as Real ;
len a >= 0 + 1 by A1, A2, NAT_1:13;
then (len a) - 1 >= 0 by XREAL_1:48;
then A20: (len a) -' 1 = (len a) - 1 by XREAL_0:def 2;
( 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 A21: i < nn ; :: thesis: q . (i + 1) = (q . i) + ((a . (i + 1)) * (b . (i + 1)))
nn + 1 <= len a by A2, NAT_1:13;
then (nn + 1) - 1 <= (len a) - 1 by XREAL_1:9;
then i < (len a) -' 1 by A20, A21, XXREAL_0:2;
hence q . (i + 1) = (q . i) + ((a . (i + 1)) * (b . (i + 1))) by A19, A21; :: thesis: verum

end;

end;

then 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))) ) & ss2 = s . n ) by A18, A20;
hence ex b₁ being Real 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 ) ; :: thesis: verum