set f = U -concatenation ;
e /\ (U -concatenation) is U -concatenation -unambiguous ;
hence e /\ U is U -prefix by DefPrefix; :: thesis: verum