len W = 1 by Lm55;
then len (W .reverse()) = 1 by FINSEQ_5:def 3;
hence W .reverse() is trivial by Lm55; :: thesis: verum