reconsider f = p as Function of Bags n,the carrier of L ;
reconsider b = x as Element of Bags n by Def14;
f . b is Element of L ;
hence p . x is Element of L ; :: thesis: verum