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