a1: 1 is Element of REAL by XREAL_0:def 1;
then reconsider f = [:NAT,NAT:] --> 1 as Function of [:NAT,NAT:],REAL by FUNCOP_1:46;
( f is P-convergent & f is convergent_in_cod1 & f is convergent_in_cod2 ) by a1;
hence ex b₁ being Function of [:NAT,NAT:],REAL st
( b₁ is P-convergent & b₁ is convergent_in_cod1 & b₁ is convergent_in_cod2 ) ; :: thesis: verum