for Rseq being Function of [:NAT,NAT:],REAL st Rseq is non-decreasing holds
( ( for m being Element of NAT holds ProjMap1 (Rseq,m) is V115() ) & ( for n being Element of NAT holds ProjMap2 (Rseq,n) is V115() ) )