arctan 0 = 0 by Th35, Th41;
hence ( arctan 0 = 0 & arctan . 0 = 0 ) ; :: thesis: verum