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 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]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
reconsider k0 = k as Nat ;
assume S1[k] ; :: thesis: S1[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 ;
then A8: (q2 ^ <%qab%>) . 0 = 0 by ;
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 ;
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 ;
case A13: k2 < k ; :: thesis: (q2 ^ <%qab%>) . (k2 + 1) = ((q2 ^ <%qab%>) . k2) + ((a . (k2 + 1)) * (b . (k2 + 1)))
then k2 < len q2 by ;
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 ;
then k2 + 1 in len q2 by ;
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 ;
k2 < k2 + 1 by NAT_1:13;
then k2 in dom q2 by ;
hence (q2 ^ <%qab%>) . (k2 + 1) = ((q2 ^ <%qab%>) . k2) + ((a . (k2 + 1)) * (b . (k2 + 1))) by ; :: 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 ;
hence S1[k + 1] by A8, A9; :: thesis: verum
end;
( len q0 = 1 & q0 . 0 = In (0,REAL) ) by AFINSQ_1:def 4;
then A17: S1[ 0 ] by A3;
for k being Nat holds S1[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 ;
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 ;
then (nn + 1) - 1 <= (len a) - 1 by XREAL_1:9;
then i < (len a) -' 1 by ;
hence q . (i + 1) = (q . i) + ((a . (i + 1)) * (b . (i + 1))) by ; :: 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 ;
hence ex b1 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))) ) & b1 = s . n ) ; :: thesis: verum