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