let r be Element of REAL ; :: thesis: ( [:NAT,NAT:] --> r is P-convergent & [:NAT,NAT:] --> r is convergent_in_cod1 & [:NAT,NAT:] --> r is convergent_in_cod2 )
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;

a3: 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;

b1: now :: thesis: for m being Element of NAT holds ProjMap2 (([:NAT,NAT:] --> r),m) is convergent

let m be Element of NAT ; :: thesis: ProjMap2 (([:NAT,NAT:] --> r),m) is convergent

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

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

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

let n be Nat; :: thesis: ( 0 <= n implies |.(((ProjMap2 (([:NAT,NAT:] --> r),m)) . n) - r).| < e )
assume 0 <= n ; :: thesis: |.(((ProjMap2 (([:NAT,NAT:] --> r),m)) . n) - r).| < e
b4: n is Element of NAT by ORDINAL1:def 12;
then (ProjMap2 (([:NAT,NAT:] --> r),m)) . n = ([:NAT,NAT:] --> r) . (n,m) by MESFUNC9:def 7;
then (ProjMap2 (([:NAT,NAT:] --> r),m)) . n = r by b4, FUNCOP_1:70;
hence |.(((ProjMap2 (([:NAT,NAT:] --> r),m)) . n) - r).| < e by b3, ABSVALUE:2; :: thesis: verum

end;

hence ex N being Nat st
for n being Nat st N <= n holds
|.(((ProjMap2 (([:NAT,NAT:] --> r),m)) . n) - r).| < e ; :: thesis: verum

end;

hence ProjMap2 (([:NAT,NAT:] --> r),m) is convergent by SEQ_2:def 6; :: thesis: verum

end;

now :: thesis: for n being Element of NAT holds ProjMap1 (([:NAT,NAT:] --> r),n) is convergent

let n be Element of NAT ; :: thesis: ProjMap1 (([:NAT,NAT:] --> r),n) is convergent

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

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

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

let m be Nat; :: thesis: ( 0 <= m implies |.(((ProjMap1 (([:NAT,NAT:] --> r),n)) . m) - r).| < e )
assume 0 <= m ; :: thesis: |.(((ProjMap1 (([:NAT,NAT:] --> r),n)) . m) - r).| < e
c4: m is Element of NAT by ORDINAL1:def 12;
then (ProjMap1 (([:NAT,NAT:] --> r),n)) . m = ([:NAT,NAT:] --> r) . (n,m) by MESFUNC9:def 6;
then (ProjMap1 (([:NAT,NAT:] --> r),n)) . m = r by c4, FUNCOP_1:70;
hence |.(((ProjMap1 (([:NAT,NAT:] --> r),n)) . m) - r).| < e by c3, ABSVALUE:2; :: thesis: verum

end;

hence ex M being Nat st
for m being Nat st M <= m holds
|.(((ProjMap1 (([:NAT,NAT:] --> r),n)) . m) - r).| < e ; :: thesis: verum

end;

hence ProjMap1 (([:NAT,NAT:] --> r),n) is convergent by SEQ_2:def 6; :: thesis: verum

end;

hence ( [:NAT,NAT:] --> r is P-convergent & [:NAT,NAT:] --> r is convergent_in_cod1 & [:NAT,NAT:] --> r is convergent_in_cod2 ) by a3, b1; :: thesis: verum