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

now :: thesis:

hereby :: thesis:

assume A1: f is convergent_in_cod1_to_+infty ; :: thesis:

now :: thesis:

let m be Element of NAT ; :: thesis:
ProjMap2 (f,m) = ProjMap1 ((~ f),m) by Th33;
hence ProjMap1 ((~ f),m) is convergent_to_+infty by A1; :: thesis:

end;

hence ~ f is convergent_in_cod2_to_+infty ; :: thesis:

end;

assume A2: ~ f is convergent_in_cod2_to_+infty ; :: thesis:

now :: thesis:

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

end;

hence f is convergent_in_cod1_to_+infty ; :: thesis:

end;

hence ( f is convergent_in_cod1_to_+infty iff ~ f is convergent_in_cod2_to_+infty ) ; :: thesis:

now :: thesis:

hereby :: thesis:

assume A3: f is convergent_in_cod2_to_+infty ; :: thesis:

now :: thesis:

let m be Element of NAT ; :: thesis:
ProjMap1 (f,m) = ProjMap2 ((~ f),m) by Th32;
hence ProjMap2 ((~ f),m) is convergent_to_+infty by A3; :: thesis:

end;

hence ~ f is convergent_in_cod1_to_+infty ; :: thesis:

end;

assume A4: ~ f is convergent_in_cod1_to_+infty ; :: thesis:

now :: thesis:

let m be Element of NAT ; :: thesis:
ProjMap1 (f,m) = ProjMap2 ((~ f),m) by Th32;
hence ProjMap1 (f,m) is convergent_to_+infty by A4; :: thesis:

end;

hence f is convergent_in_cod2_to_+infty ; :: thesis:

end;

hence ( f is convergent_in_cod2_to_+infty iff ~ f is convergent_in_cod1_to_+infty ) ; :: thesis:

now :: thesis:

hereby :: thesis:

assume A5: f is convergent_in_cod1_to_-infty ; :: thesis:

now :: thesis:

let m be Element of NAT ; :: thesis:
ProjMap2 (f,m) = ProjMap1 ((~ f),m) by Th33;
hence ProjMap1 ((~ f),m) is convergent_to_-infty by A5; :: thesis:

end;

hence ~ f is convergent_in_cod2_to_-infty ; :: thesis:

end;

assume A6: ~ f is convergent_in_cod2_to_-infty ; :: thesis:

now :: thesis:

let m be Element of NAT ; :: thesis:
ProjMap2 (f,m) = ProjMap1 ((~ f),m) by Th33;
hence ProjMap2 (f,m) is convergent_to_-infty by A6; :: thesis:

end;

hence f is convergent_in_cod1_to_-infty ; :: thesis:

end;

hence ( f is convergent_in_cod1_to_-infty iff ~ f is convergent_in_cod2_to_-infty ) ; :: thesis:

now :: thesis:

hereby :: thesis:

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

now :: thesis:

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

end;

hence ~ f is convergent_in_cod1_to_-infty ; :: thesis:

end;

assume A8: ~ f is convergent_in_cod1_to_-infty ; :: thesis:

now :: thesis:

let m be Element of NAT ; :: thesis:
ProjMap1 (f,m) = ProjMap2 ((~ f),m) by Th32;
hence ProjMap1 (f,m) is convergent_to_-infty by A8; :: thesis:

end;

hence f is convergent_in_cod2_to_-infty ; :: thesis:

end;

hence ( f is convergent_in_cod2_to_-infty iff ~ f is convergent_in_cod1_to_-infty ) ; :: thesis:

now :: thesis:

hereby :: thesis:

assume A9: f is convergent_in_cod1_to_finite ; :: thesis:

now :: thesis:

let m be Element of NAT ; :: thesis:
ProjMap2 (f,m) = ProjMap1 ((~ f),m) by Th33;
hence ProjMap1 ((~ f),m) is convergent_to_finite_number by A9; :: thesis:

end;

hence ~ f is convergent_in_cod2_to_finite ; :: thesis:

end;

assume A10: ~ f is convergent_in_cod2_to_finite ; :: thesis:

now :: thesis:

let m be Element of NAT ; :: thesis:
ProjMap2 (f,m) = ProjMap1 ((~ f),m) by Th33;
hence ProjMap2 (f,m) is convergent_to_finite_number by A10; :: thesis:

end;

hence f is convergent_in_cod1_to_finite ; :: thesis:

end;

hence ( f is convergent_in_cod1_to_finite iff ~ f is convergent_in_cod2_to_finite ) ; :: thesis:

now :: thesis:

hereby :: thesis:

assume A11: f is convergent_in_cod2_to_finite ; :: thesis:

now :: thesis:

let m be Element of NAT ; :: thesis:
ProjMap1 (f,m) = ProjMap2 ((~ f),m) by Th32;
hence ProjMap2 ((~ f),m) is convergent_to_finite_number by A11; :: thesis:

end;

hence ~ f is convergent_in_cod1_to_finite ; :: thesis:

end;

assume A12: ~ f is convergent_in_cod1_to_finite ; :: thesis:

now :: thesis:

let m be Element of NAT ; :: thesis:
ProjMap1 (f,m) = ProjMap2 ((~ f),m) by Th32;
hence ProjMap1 (f,m) is convergent_to_finite_number by A12; :: thesis:

end;

hence f is convergent_in_cod2_to_finite ; :: thesis:

end;

hence ( f is convergent_in_cod2_to_finite iff ~ f is convergent_in_cod1_to_finite ) ; :: thesis: