((0. X),(0. X)) to_power 1 = 0. X by Th6;
hence 0. X is nilpotent ; :: thesis: verum