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

now :: thesis: ( ( f is convergent_in_cod1_to_+infty implies ~ f is convergent_in_cod2_to_+infty ) & ( ~ f is convergent_in_cod2_to_+infty implies f is convergent_in_cod1_to_+infty ) )

hereby :: thesis: ( ~ f is convergent_in_cod2_to_+infty implies f is convergent_in_cod1_to_+infty )

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

now :: thesis: for m being Element of NAT holds ProjMap1 ((~ f),m) is convergent_to_+infty

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

end;

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

end;

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

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

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

end;

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

end;

hence ( f is convergent_in_cod1_to_+infty iff ~ f is convergent_in_cod2_to_+infty ) ; :: thesis: ( ( f is convergent_in_cod2_to_+infty implies ~ f is convergent_in_cod1_to_+infty ) & ( ~ f is convergent_in_cod1_to_+infty implies f is convergent_in_cod2_to_+infty ) & ( f is convergent_in_cod1_to_-infty implies ~ f is convergent_in_cod2_to_-infty ) & ( ~ f is convergent_in_cod2_to_-infty implies f is convergent_in_cod1_to_-infty ) & ( f is convergent_in_cod2_to_-infty implies ~ f is convergent_in_cod1_to_-infty ) & ( ~ f is convergent_in_cod1_to_-infty implies f is convergent_in_cod2_to_-infty ) & ( f is convergent_in_cod1_to_finite implies ~ f is convergent_in_cod2_to_finite ) & ( ~ f is convergent_in_cod2_to_finite implies f is convergent_in_cod1_to_finite ) & ( f is convergent_in_cod2_to_finite implies ~ f is convergent_in_cod1_to_finite ) & ( ~ f is convergent_in_cod1_to_finite implies f is convergent_in_cod2_to_finite ) )

now :: thesis: ( ( f is convergent_in_cod2_to_+infty implies ~ f is convergent_in_cod1_to_+infty ) & ( ~ f is convergent_in_cod1_to_+infty implies f is convergent_in_cod2_to_+infty ) )

hereby :: thesis: ( ~ f is convergent_in_cod1_to_+infty implies f is convergent_in_cod2_to_+infty )

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

now :: thesis: for m being Element of NAT holds ProjMap2 ((~ f),m) is convergent_to_+infty

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

end;

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

end;

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

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

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

end;

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

end;

hence ( f is convergent_in_cod2_to_+infty iff ~ f is convergent_in_cod1_to_+infty ) ; :: thesis: ( ( f is convergent_in_cod1_to_-infty implies ~ f is convergent_in_cod2_to_-infty ) & ( ~ f is convergent_in_cod2_to_-infty implies f is convergent_in_cod1_to_-infty ) & ( f is convergent_in_cod2_to_-infty implies ~ f is convergent_in_cod1_to_-infty ) & ( ~ f is convergent_in_cod1_to_-infty implies f is convergent_in_cod2_to_-infty ) & ( f is convergent_in_cod1_to_finite implies ~ f is convergent_in_cod2_to_finite ) & ( ~ f is convergent_in_cod2_to_finite implies f is convergent_in_cod1_to_finite ) & ( f is convergent_in_cod2_to_finite implies ~ f is convergent_in_cod1_to_finite ) & ( ~ f is convergent_in_cod1_to_finite implies f is convergent_in_cod2_to_finite ) )

now :: thesis: ( ( f is convergent_in_cod1_to_-infty implies ~ f is convergent_in_cod2_to_-infty ) & ( ~ f is convergent_in_cod2_to_-infty implies f is convergent_in_cod1_to_-infty ) )

hereby :: thesis: ( ~ f is convergent_in_cod2_to_-infty implies f is convergent_in_cod1_to_-infty )

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

now :: thesis: for m being Element of NAT holds ProjMap1 ((~ f),m) is convergent_to_-infty

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

end;

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

end;

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

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

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

end;

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

end;

hence ( f is convergent_in_cod1_to_-infty iff ~ f is convergent_in_cod2_to_-infty ) ; :: thesis: ( ( f is convergent_in_cod2_to_-infty implies ~ f is convergent_in_cod1_to_-infty ) & ( ~ f is convergent_in_cod1_to_-infty implies f is convergent_in_cod2_to_-infty ) & ( f is convergent_in_cod1_to_finite implies ~ f is convergent_in_cod2_to_finite ) & ( ~ f is convergent_in_cod2_to_finite implies f is convergent_in_cod1_to_finite ) & ( f is convergent_in_cod2_to_finite implies ~ f is convergent_in_cod1_to_finite ) & ( ~ f is convergent_in_cod1_to_finite implies f is convergent_in_cod2_to_finite ) )

now :: thesis: ( ( f is convergent_in_cod2_to_-infty implies ~ f is convergent_in_cod1_to_-infty ) & ( ~ f is convergent_in_cod1_to_-infty implies f is convergent_in_cod2_to_-infty ) )

hereby :: thesis: ( ~ f is convergent_in_cod1_to_-infty implies f is convergent_in_cod2_to_-infty )

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

now :: thesis: for m being Element of NAT holds ProjMap2 ((~ f),m) is convergent_to_-infty

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

end;

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

end;

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

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

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

end;

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

end;

hence ( f is convergent_in_cod2_to_-infty iff ~ f is convergent_in_cod1_to_-infty ) ; :: thesis: ( ( f is convergent_in_cod1_to_finite implies ~ f is convergent_in_cod2_to_finite ) & ( ~ f is convergent_in_cod2_to_finite implies f is convergent_in_cod1_to_finite ) & ( f is convergent_in_cod2_to_finite implies ~ f is convergent_in_cod1_to_finite ) & ( ~ f is convergent_in_cod1_to_finite implies f is convergent_in_cod2_to_finite ) )

now :: thesis: ( ( f is convergent_in_cod1_to_finite implies ~ f is convergent_in_cod2_to_finite ) & ( ~ f is convergent_in_cod2_to_finite implies f is convergent_in_cod1_to_finite ) )

hereby :: thesis: ( ~ f is convergent_in_cod2_to_finite implies f is convergent_in_cod1_to_finite )

assume A9: f is convergent_in_cod1_to_finite ; :: thesis: ~ f is convergent_in_cod2_to_finite

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

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

end;

hence ~ f is convergent_in_cod2_to_finite ; :: thesis: verum

end;

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

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

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

end;

hence f is convergent_in_cod1_to_finite ; :: thesis: verum

end;

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

now :: thesis: ( ( f is convergent_in_cod2_to_finite implies ~ f is convergent_in_cod1_to_finite ) & ( ~ f is convergent_in_cod1_to_finite implies f is convergent_in_cod2_to_finite ) )

hereby :: thesis: ( ~ f is convergent_in_cod1_to_finite implies f is convergent_in_cod2_to_finite )

assume A11: f is convergent_in_cod2_to_finite ; :: thesis: ~ f is convergent_in_cod1_to_finite

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

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

end;

hence ~ f is convergent_in_cod1_to_finite ; :: thesis: verum

end;

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

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

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

end;

hence f is convergent_in_cod2_to_finite ; :: thesis: verum

end;

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