let f be Function of [:NAT,NAT:],ExtREAL; :: thesis:

hereby :: thesis:

assume A1: ( f is convergent_in_cod1_to_+infty or f is convergent_in_cod1_to_-infty or f is convergent_in_cod1_to_finite ) ; :: thesis:

per cases by A1;

suppose A2: f is convergent_in_cod1_to_+infty ; :: thesis:

now :: thesis:

let m be Element of NAT ; :: thesis:
ProjMap2 (f,m) is convergent_to_+infty by A2;
hence ProjMap2 (f,m) is convergent ; :: thesis:

end;

hence f is convergent_in_cod1 ; :: thesis:

end;

suppose A3: f is convergent_in_cod1_to_-infty ; :: thesis:

now :: thesis:

let m be Element of NAT ; :: thesis:
ProjMap2 (f,m) is convergent_to_-infty by A3;
hence ProjMap2 (f,m) is convergent ; :: thesis:

end;

hence f is convergent_in_cod1 ; :: thesis:

end;

suppose A4: f is convergent_in_cod1_to_finite ; :: thesis:

now :: thesis:

let m be Element of NAT ; :: thesis:
ProjMap2 (f,m) is convergent_to_finite_number by A4;
hence ProjMap2 (f,m) is convergent ; :: thesis:

end;

hence f is convergent_in_cod1 ; :: thesis:

end;

end;

end;

assume A5: ( f is convergent_in_cod2_to_+infty or f is convergent_in_cod2_to_-infty or f is convergent_in_cod2_to_finite ) ; :: thesis:

per cases by A5;

suppose A6: f is convergent_in_cod2_to_+infty ; :: thesis:

now :: thesis:

let m be Element of NAT ; :: thesis:
ProjMap1 (f,m) is convergent_to_+infty by A6;
hence ProjMap1 (f,m) is convergent ; :: thesis:

end;

hence f is convergent_in_cod2 ; :: thesis:

end;

suppose A7: f is convergent_in_cod2_to_-infty ; :: thesis:

now :: thesis:

let m be Element of NAT ; :: thesis:
ProjMap1 (f,m) is convergent_to_-infty by A7;
hence ProjMap1 (f,m) is convergent ; :: thesis:

end;

hence f is convergent_in_cod2 ; :: thesis:

end;

suppose A8: f is convergent_in_cod2_to_finite ; :: thesis:

now :: thesis:

let m be Element of NAT ; :: thesis:
ProjMap1 (f,m) is convergent_to_finite_number by A8;
hence ProjMap1 (f,m) is convergent ; :: thesis:

end;

hence f is convergent_in_cod2 ; :: thesis:

end;

end;