thus for w1, w2 being Real st ex s being XFinSequence of REAL ex n1 being Integer st
( len s = len a & s . 0 = 0 & n1 = b . 0 & ( n1 <> 0 implies for i being Nat st i < n1 holds
s . (i + 1) = (s . i) + ((a . (i + 1)) * (b . (i + 1))) ) & w1 = s . n1 ) & ex s being XFinSequence of REAL ex n2 being Integer st
( len s = len a & s . 0 = 0 & n2 = b . 0 & ( n2 <> 0 implies for i being Nat st i < n2 holds
s . (i + 1) = (s . i) + ((a . (i + 1)) * (b . (i + 1))) ) & w2 = s . n2 ) holds
w1 = w2 :: thesis: verum
proof
let w1, w2 be Real; :: thesis: ( ex s being XFinSequence of REAL ex n1 being Integer st
( len s = len a & s . 0 = 0 & n1 = b . 0 & ( n1 <> 0 implies for i being Nat st i < n1 holds
s . (i + 1) = (s . i) + ((a . (i + 1)) * (b . (i + 1))) ) & w1 = s . n1 ) & ex s being XFinSequence of REAL ex n2 being Integer st
( len s = len a & s . 0 = 0 & n2 = b . 0 & ( n2 <> 0 implies for i being Nat st i < n2 holds
s . (i + 1) = (s . i) + ((a . (i + 1)) * (b . (i + 1))) ) & w2 = s . n2 ) implies w1 = w2 )
assume that
A22: ex s being XFinSequence of REAL ex n1 being Integer st
( len s = len a & s . 0 = 0 & n1 = b . 0 & ( n1 <> 0 implies for i being Nat st i < n1 holds
s . (i + 1) = (s . i) + ((a . (i + 1)) * (b . (i + 1))) ) & w1 = s . n1 ) and
A23: ex s being XFinSequence of REAL ex n2 being Integer st
( len s = len a & s . 0 = 0 & n2 = b . 0 & ( n2 <> 0 implies for i being Nat st i < n2 holds
s . (i + 1) = (s . i) + ((a . (i + 1)) * (b . (i + 1))) ) & w2 = s . n2 ) ; :: thesis: w1 = w2
consider s1 being XFinSequence of REAL , n1 being Integer such that
len s1 = len a and
A24: s1 . 0 = 0 and
A25: n1 = b . 0 and
A26: ( n1 <> 0 implies for i being Nat st i < n1 holds
s1 . (i + 1) = (s1 . i) + ((a . (i + 1)) * (b . (i + 1))) ) and
A27: w1 = s1 . n1 by A22;
consider s2 being XFinSequence of REAL , n2 being Integer such that
len s2 = len a and
A28: s2 . 0 = 0 and
A29: n2 = b . 0 and
A30: ( n2 <> 0 implies for i being Nat st i < n2 holds
s2 . (i + 1) = (s2 . i) + ((a . (i + 1)) * (b . (i + 1))) ) and
A31: w2 = s2 . n2 by A23;
reconsider n = n1 as Nat by A1, A25;
defpred S1[ Nat] means ( $1 <= n implies s1 . $1 = s2 . $1 );
A32: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A33: S1[k] ; :: thesis: S1[k + 1]
now :: thesis: ( k + 1 <= n implies s1 . (k + 1) = s2 . (k + 1) )
assume k + 1 <= n ; :: thesis: s1 . (k + 1) = s2 . (k + 1)
then A34: k < n by NAT_1:13;
then s1 . (k + 1) = (s1 . k) + ((a . (k + 1)) * (b . (k + 1))) by A26;
hence s1 . (k + 1) = s2 . (k + 1) by A25, A29, A30, A33, A34; :: thesis: verum
end;
hence S1[k + 1] ; :: thesis: verum
end;
A35: S1[ 0 ] by A24, A28;
for k being Nat holds S1[k] from NAT_1:sch 2(A35, A32);
 hence w1 = w2 by A25, A27, A29, A31; :: thesis: verum
end;