Pseq2 is P-convergent ;
then consider z being Real such that
a3: for e being Real st 0 < e holds
ex N1 being Nat st
for n, m being Nat st n >= N1 & m >= N1 holds
|.((Pseq2 . (n,m)) - z).| < e ;
for e being Real st 0 < e holds
ex N being Nat st
for n being Nat st n >= N holds
|.(((lim_in_cod2 Pseq2) . n) - z).| < e
proof
let e be Real; :: thesis: ( 0 < e implies ex N being Nat st
for n being Nat st n >= N holds
|.(((lim_in_cod2 Pseq2) . n) - z).| < e )
assume a8: 0 < e ; :: thesis: ex N being Nat st
for n being Nat st n >= N holds
|.(((lim_in_cod2 Pseq2) . n) - z).| < e
then consider N1 being Nat such that
a15: for n, m being Nat st n >= N1 & m >= N1 holds
|.((Pseq2 . (n,m)) - z).| < e / 2 by a3;
a12: for n being Element of NAT st n >= N1 holds
ex N2 being Nat st
for m being Nat st m >= N2 holds
|.(((ProjMap1 (Pseq2,n)) . m) - ((lim_in_cod2 Pseq2) . n)).| < e / 2
proof
let n be Element of NAT ; :: thesis: ( n >= N1 implies ex N2 being Nat st
for m being Nat st m >= N2 holds
|.(((ProjMap1 (Pseq2,n)) . m) - ((lim_in_cod2 Pseq2) . n)).| < e / 2 )
assume n >= N1 ; :: thesis: ex N2 being Nat st
for m being Nat st m >= N2 holds
|.(((ProjMap1 (Pseq2,n)) . m) - ((lim_in_cod2 Pseq2) . n)).| < e / 2
Pseq2 is convergent_in_cod2 ;
then ProjMap1 (Pseq2,n) is convergent ;
then consider N2 being Nat such that
a9: for m being Nat st m >= N2 holds
|.(((ProjMap1 (Pseq2,n)) . m) - (lim (ProjMap1 (Pseq2,n)))).| < e / 2 by a8, SEQ_2:def 7;
take N2 ; :: thesis: for m being Nat st m >= N2 holds
|.(((ProjMap1 (Pseq2,n)) . m) - ((lim_in_cod2 Pseq2) . n)).| < e / 2
thus for m being Nat st m >= N2 holds
|.(((ProjMap1 (Pseq2,n)) . m) - ((lim_in_cod2 Pseq2) . n)).| < e / 2 :: thesis: verum
proof
let m be Nat; :: thesis: ( m >= N2 implies |.(((ProjMap1 (Pseq2,n)) . m) - ((lim_in_cod2 Pseq2) . n)).| < e / 2 )
assume m >= N2 ; :: thesis: |.(((ProjMap1 (Pseq2,n)) . m) - ((lim_in_cod2 Pseq2) . n)).| < e / 2
then |.(((ProjMap1 (Pseq2,n)) . m) - (lim (ProjMap1 (Pseq2,n)))).| < e / 2 by a9;
hence |.(((ProjMap1 (Pseq2,n)) . m) - ((lim_in_cod2 Pseq2) . n)).| < e / 2 by def33; :: thesis: verum
end;
end;
take N1 ; :: thesis: for n being Nat st n >= N1 holds
|.(((lim_in_cod2 Pseq2) . n) - z).| < e
thus for n being Nat st n >= N1 holds
|.(((lim_in_cod2 Pseq2) . n) - z).| < e :: thesis: verum
proof
let n be Nat; :: thesis: ( n >= N1 implies |.(((lim_in_cod2 Pseq2) . n) - z).| < e )
reconsider n1 = n as Element of NAT by ORDINAL1:def 12;
assume a14: n >= N1 ; :: thesis: |.(((lim_in_cod2 Pseq2) . n) - z).| < e
then consider N2 being Nat such that
a13: for m being Nat st m >= N2 holds
|.(((ProjMap1 (Pseq2,n1)) . m) - ((lim_in_cod2 Pseq2) . n1)).| < e / 2 by a12;
reconsider M = max (N2,N1) as Element of NAT by ORDINAL1:def 12;
a17: (ProjMap1 (Pseq2,n1)) . M = Pseq2 . (n,M) by MESFUNC9:def 6;
a16: ( M >= N2 & M >= N1 ) by XXREAL_0:25;
a18: |.(((lim_in_cod2 Pseq2) . n) - z).| <= |.(((lim_in_cod2 Pseq2) . n) - ((ProjMap1 (Pseq2,n1)) . M)).| + |.((Pseq2 . (n,M)) - z).| by a17, COMPLEX1:63;
|.(((lim_in_cod2 Pseq2) . n) - ((ProjMap1 (Pseq2,n1)) . M)).| = |.(((ProjMap1 (Pseq2,n1)) . M) - ((lim_in_cod2 Pseq2) . n)).| by COMPLEX1:60;
then a20: |.(((lim_in_cod2 Pseq2) . n) - ((ProjMap1 (Pseq2,n1)) . M)).| < e / 2 by a13, XXREAL_0:25;
|.((Pseq2 . (n1,M)) - z).| < e / 2 by a15, a16, a14;
then |.(((lim_in_cod2 Pseq2) . n) - ((ProjMap1 (Pseq2,n1)) . M)).| + |.((Pseq2 . (n,M)) - z).| < (e / 2) + (e / 2) by a20, XREAL_1:8;
hence |.(((lim_in_cod2 Pseq2) . n) - z).| < e by a18, XXREAL_0:2; :: thesis: verum
end;
end;
hence lim_in_cod2 Pseq2 is convergent by SEQ_2:def 6; :: thesis: verum