l . x in [#] F ;
hence l . x is Element of F ; :: thesis: verum