set W = W1 .append W2;

now :: thesis: W1 .append W2 is trivial

per cases ( W1 .last() = W2 .first() or W1 .last() <> W2 .first() ) ;

suppose W1 .last() = W2 .first() ; :: thesis: W1 .append W2 is trivial

then (len (W1 .append W2)) + 1 = (len W1) + (len W2) by Lm9
.= (len W1) + 1 by Lm55
.= 1 + 1 by Lm55 ;
hence W1 .append W2 is trivial by Lm55; :: thesis: verum

end;

suppose W1 .last() <> W2 .first() ; :: thesis: W1 .append W2 is trivial

hence W1 .append W2 is trivial by Def10; :: thesis: verum

end;

end;

end;

hence W1 .append W2 is trivial ; :: thesis: verum