(0._ L) `1 = 0_. L by XTUPLE_0:def 2;
hence 0._ L is zero by defzerrat; :: thesis: verum