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:
A2: ProjMap2 (f,m) is convergent_to_+infty by A1;
- (ProjMap2 (f,m)) = ProjMap2 ((- f),m) by Th35;
hence ProjMap2 ((- f),m) is convergent_to_-infty by A2, Th17; :: thesis:

end;

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

end;

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

now :: thesis:

let m be Element of NAT ; :: thesis:
- (ProjMap2 (f,m)) = ProjMap2 ((- f),m) by Th35;
then - (ProjMap2 (f,m)) is convergent_to_-infty by A3;
then - (- (ProjMap2 (f,m))) is convergent_to_+infty by Th17;
hence ProjMap2 (f,m) is convergent_to_+infty by Th2; :: 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_cod1_to_-infty ) ; :: thesis:

now :: thesis:

hereby :: thesis:

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

now :: thesis:

let m be Element of NAT ; :: thesis:
A2: ProjMap2 (f,m) is convergent_to_-infty by A1;
- (ProjMap2 (f,m)) = ProjMap2 ((- f),m) by Th35;
hence ProjMap2 ((- f),m) is convergent_to_+infty by A2, Th17; :: thesis:

end;

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

end;

assume A3: - f is convergent_in_cod1_to_+infty ; :: thesis:

now :: thesis:

let m be Element of NAT ; :: thesis:
- (ProjMap2 (f,m)) = ProjMap2 ((- f),m) by Th35;
then - (ProjMap2 (f,m)) is convergent_to_+infty by A3;
then - (- (ProjMap2 (f,m))) is convergent_to_-infty by Th17;
hence ProjMap2 (f,m) is convergent_to_-infty by Th2; :: 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_cod1_to_+infty ) ; :: thesis:

now :: thesis:

hereby :: thesis:

assume A1: f is convergent_in_cod1_to_finite ; :: thesis:

now :: thesis:

let m be Element of NAT ; :: thesis:
A2: ProjMap2 (f,m) is convergent_to_finite_number by A1;
- (ProjMap2 (f,m)) = ProjMap2 ((- f),m) by Th35;
hence ProjMap2 ((- f),m) is convergent_to_finite_number by A2, Th17; :: thesis:

end;

hence - f is convergent_in_cod1_to_finite ; :: thesis:

end;

assume A3: - f is convergent_in_cod1_to_finite ; :: thesis:

now :: thesis:

let m be Element of NAT ; :: thesis:
- (ProjMap2 (f,m)) = ProjMap2 ((- f),m) by Th35;
then - (ProjMap2 (f,m)) is convergent_to_finite_number by A3;
then - (- (ProjMap2 (f,m))) is convergent_to_finite_number by Th17;
hence ProjMap2 (f,m) is convergent_to_finite_number by Th2; :: 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_cod1_to_finite ) ; :: thesis:

now :: thesis:

hereby :: thesis:

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

now :: thesis:

let m be Element of NAT ; :: thesis:
A2: ProjMap1 (f,m) is convergent_to_+infty by A1;
- (ProjMap1 (f,m)) = ProjMap1 ((- f),m) by Th34;
hence ProjMap1 ((- f),m) is convergent_to_-infty by A2, Th17; :: thesis:

end;

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

end;

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

now :: thesis:

let m be Element of NAT ; :: thesis:
- (ProjMap1 (f,m)) = ProjMap1 ((- f),m) by Th34;
then - (ProjMap1 (f,m)) is convergent_to_-infty by A3;
then - (- (ProjMap1 (f,m))) is convergent_to_+infty by Th17;
hence ProjMap1 (f,m) is convergent_to_+infty by Th2; :: 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_cod2_to_-infty ) ; :: thesis:

now :: thesis:

hereby :: thesis:

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

now :: thesis:

let m be Element of NAT ; :: thesis:
A2: ProjMap1 (f,m) is convergent_to_-infty by A1;
- (ProjMap1 (f,m)) = ProjMap1 ((- f),m) by Th34;
hence ProjMap1 ((- f),m) is convergent_to_+infty by A2, Th17; :: thesis:

end;

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

end;

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

now :: thesis:

let m be Element of NAT ; :: thesis:
- (ProjMap1 (f,m)) = ProjMap1 ((- f),m) by Th34;
then - (ProjMap1 (f,m)) is convergent_to_+infty by A3;
then - (- (ProjMap1 (f,m))) is convergent_to_-infty by Th17;
hence ProjMap1 (f,m) is convergent_to_-infty by Th2; :: 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_cod2_to_+infty ) ; :: thesis:

now :: thesis:

hereby :: thesis:

assume A1: f is convergent_in_cod2_to_finite ; :: thesis:

now :: thesis:

let m be Element of NAT ; :: thesis:
A2: ProjMap1 (f,m) is convergent_to_finite_number by A1;
- (ProjMap1 (f,m)) = ProjMap1 ((- f),m) by Th34;
hence ProjMap1 ((- f),m) is convergent_to_finite_number by A2, Th17; :: thesis:

end;

hence - f is convergent_in_cod2_to_finite ; :: thesis:

end;

assume A3: - f is convergent_in_cod2_to_finite ; :: thesis:

now :: thesis:

let m be Element of NAT ; :: thesis:
- (ProjMap1 (f,m)) = ProjMap1 ((- f),m) by Th34;
then - (ProjMap1 (f,m)) is convergent_to_finite_number by A3;
then - (- (ProjMap1 (f,m))) is convergent_to_finite_number by Th17;
hence ProjMap1 (f,m) is convergent_to_finite_number by Th2; :: 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_cod2_to_finite ) ; :: thesis: