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