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 ;
hence p . x is Element of ; :: thesis: verum