let f be Function of [:NAT,NAT:],ExtREAL; :: thesis: ( ( ( f is convergent_in_cod1_to_+infty or f is convergent_in_cod1_to_-infty or f is convergent_in_cod1_to_finite ) implies f is convergent_in_cod1 ) & ( ( f is convergent_in_cod2_to_+infty or f is convergent_in_cod2_to_-infty or f is convergent_in_cod2_to_finite ) implies f is convergent_in_cod2 ) )

hereby :: thesis: ( ( f is convergent_in_cod2_to_+infty or f is convergent_in_cod2_to_-infty or f is convergent_in_cod2_to_finite ) implies f is convergent_in_cod2 )

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: f is convergent_in_cod1

per cases ( f is convergent_in_cod1_to_+infty or f is convergent_in_cod1_to_-infty or f is convergent_in_cod1_to_finite ) by A1;

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

now :: thesis: for m being Element of NAT holds ProjMap2 (f,m) is convergent

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

end;

hence f is convergent_in_cod1 ; :: thesis: verum

end;

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

now :: thesis: for m being Element of NAT holds ProjMap2 (f,m) is convergent

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

end;

hence f is convergent_in_cod1 ; :: thesis: verum

end;

suppose A4: f is convergent_in_cod1_to_finite ; :: thesis: f is convergent_in_cod1

now :: thesis: for m being Element of NAT holds ProjMap2 (f,m) is convergent

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

end;

hence f is convergent_in_cod1 ; :: thesis: verum

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: f is convergent_in_cod2

per cases ( f is convergent_in_cod2_to_+infty or f is convergent_in_cod2_to_-infty or f is convergent_in_cod2_to_finite ) by A5;

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

now :: thesis: for m being Element of NAT holds ProjMap1 (f,m) is convergent

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

end;

hence f is convergent_in_cod2 ; :: thesis: verum

end;

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

now :: thesis: for m being Element of NAT holds ProjMap1 (f,m) is convergent

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

end;

hence f is convergent_in_cod2 ; :: thesis: verum

end;

suppose A8: f is convergent_in_cod2_to_finite ; :: thesis: f is convergent_in_cod2

now :: thesis: for m being Element of NAT holds ProjMap1 (f,m) is convergent

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

end;

hence f is convergent_in_cod2 ; :: thesis: verum

end;

end;