thus for w1, w2 being Real st ex s being XFinSequence of 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 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 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 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 A19: ( ex s being XFinSequence of 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 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
then consider s1 being XFinSequence of , n1 being Integer such that
A20: ( len s1 = len a & s1 . 0 = 0 & n1 = b . 0 & ( n1 <> 0 implies for i being Nat st i < n1 holds
s1 . (i + 1) = (s1 . i) + ((a . (i + 1)) * (b . (i + 1))) ) & w1 = s1 . n1 ) ;
consider s2 being XFinSequence of , n2 being Integer such that
A21: ( len s2 = len a & s2 . 0 = 0 & n2 = b . 0 & ( n2 <> 0 implies for i being Nat st i < n2 holds
s2 . (i + 1) = (s2 . i) + ((a . (i + 1)) * (b . (i + 1))) ) & w2 = s2 . n2 ) by A19;
reconsider n = n1 as Nat by A1, A20;
defpred S₁[ Nat] means ( $1 <= n implies s1 . $1 = s2 . $1 );
A22: S₁[ 0 ] by A20, A21;
A23: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A24: S₁[k] ; :: thesis: S₁[k + 1]

now

assume k + 1 <= n ; :: thesis: s1 . (k + 1) = s2 . (k + 1)
then A25: k < n by NAT_1:13;
then s1 . (k + 1) = (s1 . k) + ((a . (k + 1)) * (b . (k + 1))) by A20;
hence s1 . (k + 1) = s2 . (k + 1) by A20, A21, A24, A25; :: thesis: verum

end;

hence S₁[k + 1] ; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A22, A23);
hence w1 = w2 by A20, A21; :: thesis: verum

end;