assume A1: the ZeroF of (Trivial-AMI N) in NAT ; :: according to COMPOS_1:def 12 :: thesis: contradiction
the ZeroF of (Trivial-AMI N) = NAT by Def1;
hence contradiction by A1; :: thesis: verum