let PS1, PS2 be Functional_Sequence of X,REAL; :: thesis: ( PS1 . 0 = F . 0 & ( for n being Nat holds PS1 . (n + 1) = (PS1 . n) + (F . (n + 1)) ) & PS2 . 0 = F . 0 & ( for n being Nat holds PS2 . (n + 1) = (PS2 . n) + (F . (n + 1)) ) implies PS1 = PS2 )

assume that

A7: PS1 . 0 = F . 0 and

A8: for n being Nat holds PS1 . (n + 1) = (PS1 . n) + (F . (n + 1)) and

A9: PS2 . 0 = F . 0 and

A10: for n being Nat holds PS2 . (n + 1) = (PS2 . n) + (F . (n + 1)) ; :: thesis: PS1 = PS2

defpred S_{1}[ Nat] means PS1 . $1 = PS2 . $1;

A11: for n being Nat st S_{1}[n] holds

S_{1}[n + 1]
_{1}[ 0 ]
by A7, A9;

for n being Nat holds S_{1}[n]
from NAT_1:sch 2(A13, A11);

then for m being Element of NAT holds PS1 . m = PS2 . m ;

hence PS1 = PS2 ; :: thesis: verum

assume that

A7: PS1 . 0 = F . 0 and

A8: for n being Nat holds PS1 . (n + 1) = (PS1 . n) + (F . (n + 1)) and

A9: PS2 . 0 = F . 0 and

A10: for n being Nat holds PS2 . (n + 1) = (PS2 . n) + (F . (n + 1)) ; :: thesis: PS1 = PS2

defpred S

A11: for n being Nat st S

S

proof

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

assume A12: S_{1}[n]
; :: thesis: S_{1}[n + 1]

PS1 . (n + 1) = (PS1 . n) + (F . (n + 1)) by A8;

hence PS1 . (n + 1) = PS2 . (n + 1) by A10, A12; :: thesis: verum

end;assume A12: S

PS1 . (n + 1) = (PS1 . n) + (F . (n + 1)) by A8;

hence PS1 . (n + 1) = PS2 . (n + 1) by A10, A12; :: thesis: verum

for n being Nat holds S

then for m being Element of NAT holds PS1 . m = PS2 . m ;

hence PS1 = PS2 ; :: thesis: verum