set l = (max ((len f),n)) - (len f);
f | (Seg ((len f) + ((max ((len f),n)) - (len f)))) = f | ((len f) + ((max ((len f),n)) - (len f))) ;
hence f | (Seg (max ((len f),n))) = f ; :: thesis: verum