let r be Element of REAL ; :: thesis: P-lim ([:NAT,NAT:] --> r) = r
set Rseq = [:NAT,NAT:] --> r;
a1: for n, m being Nat holds ([:NAT,NAT:] --> r) . (n,m) = r

proof

let n, m be Nat; :: thesis: ([:NAT,NAT:] --> r) . (n,m) = r
( n is Element of NAT & m is Element of NAT ) by ORDINAL1:def 12;
hence ([:NAT,NAT:] --> r) . (n,m) = r by FUNCOP_1:70; :: thesis: verum

end;

now :: thesis: for e being Real st 0 < e holds
ex N being Nat st
for n, m being Nat st n >= N & m >= N holds
|.((([:NAT,NAT:] --> r) . (n,m)) - r).| < e

let e be Real; :: thesis: ( 0 < e implies ex N being Nat st
for n, m being Nat st n >= N & m >= N holds
|.((([:NAT,NAT:] --> r) . (n,m)) - r).| < e )
assume a2: 0 < e ; :: thesis: ex N being Nat st
for n, m being Nat st n >= N & m >= N holds
|.((([:NAT,NAT:] --> r) . (n,m)) - r).| < e

a4: now :: thesis: for n, m being Nat st n >= 0 & m >= 0 holds
|.((([:NAT,NAT:] --> r) . (n,m)) - r).| < e

let n, m be Nat; :: thesis: ( n >= 0 & m >= 0 implies |.((([:NAT,NAT:] --> r) . (n,m)) - r).| < e )
assume ( n >= 0 & m >= 0 ) ; :: thesis: |.((([:NAT,NAT:] --> r) . (n,m)) - r).| < e
([:NAT,NAT:] --> r) . (n,m) = r by a1;
hence |.((([:NAT,NAT:] --> r) . (n,m)) - r).| < e by a2, COMPLEX1:44; :: thesis: verum

end;

reconsider N = 0 as Nat ;
take N = N; :: thesis: for n, m being Nat st n >= N & m >= N holds
|.((([:NAT,NAT:] --> r) . (n,m)) - r).| < e
thus for n, m being Nat st n >= N & m >= N holds
|.((([:NAT,NAT:] --> r) . (n,m)) - r).| < e by a4; :: thesis: verum

end;

hence P-lim ([:NAT,NAT:] --> r) = r by def6; :: thesis: verum