0 in 2 by NAT_1:45;
hence 0. Z_2 = 0 by FUNCT_7:def 1; :: thesis: verum