let PS1, PS2 be Functional_Sequence of X,COMPLEX; ( 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))
; PS1 = PS2
defpred S1[ Nat] means PS1 . $1 = PS2 . $1;
A11:
for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be
Nat;
( S1[n] implies S1[n + 1] )
assume A12:
S1[
n]
;
S1[n + 1]
PS1 . (n + 1) = (PS1 . n) + (F . (n + 1))
by A8;
hence
PS1 . (n + 1) = PS2 . (n + 1)
by A10, A12;
verum
end;
A13:
S1[ 0 ]
by A7, A9;
for n being Nat holds S1[n]
from NAT_1:sch 2(A13, A11);
then
for m being Element of NAT holds PS1 . m = PS2 . m
;
hence
PS1 = PS2
; verum