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 S₁[ Nat] means ( $1 <= n implies s1 . $1 = s2 . $1 );
A32: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A33: S₁[k] ; :: thesis: S₁[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 S₁[k + 1] ; :: thesis: verum

end;

A35: S₁[ 0 ] by A24, A28;
for k being Nat holds S₁[k] from NAT_1:sch 2(A35, A32);
hence w1 = w2 by A25, A27, A29, A31; :: thesis: verum

end;