let PS1, PS2 be Functional_Sequence of X,COMPLEX; :: 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₁[ Nat] means PS1 . $1 = PS2 . $1;
A11: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

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

A13: S₁[ 0 ] by A7, A9;
for n being Nat holds S₁[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