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

( 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_{1}[ Nat] means ( $1 <= n implies s1 . $1 = s2 . $1 );

A32: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]
_{1}[ 0 ]
by A24, A28;

for k being Nat holds S_{1}[k]
from NAT_1:sch 2(A35, A32);

hence w1 = w2 by A25, A27, A29, A31; :: thesis: verum

end;( 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

A32: for k being Nat st S

S

proof

A35:
S
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A33: S_{1}[k]
; :: thesis: S_{1}[k + 1]

_{1}[k + 1]
; :: thesis: verum

end;assume A33: S

now :: thesis: ( k + 1 <= n implies s1 . (k + 1) = s2 . (k + 1) )

hence
Sassume
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;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

for k being Nat holds S

hence w1 = w2 by A25, A27, A29, A31; :: thesis: verum