let PS1, PS2 be Functional_Sequence of X,ExtREAL; :: 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
A8: PS1 . 0 = F . 0 and
A9: for n being Nat holds PS1 . (n + 1) = (PS1 . n) + (F . (n + 1)) and
A10: PS2 . 0 = F . 0 and
A11: for n being Nat holds PS2 . (n + 1) = (PS2 . n) + (F . (n + 1)) ; :: thesis: PS1 = PS2
defpred S₁[ Nat] means PS1 . $1 = PS2 . $1;
A12: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A13: S₁[n] ; :: thesis: S₁[n + 1]
PS1 . (n + 1) = (PS1 . n) + (F . (n + 1)) by A9;
hence S₁[n + 1] by A11, A13; :: thesis: verum

end;

A14: S₁[ 0 ] by A8, A10;
for n being Nat holds S₁[n] from NAT_1:sch 2(A14, A12);
then for m being Element of NAT holds PS1 . m = PS2 . m ;
hence PS1 = PS2 ; :: thesis: verum