defpred S₁[ object , object ] means $2 = |.(p . $1).|;
A1: for x being Element of Bags n ex y being Element of F_Real st S₁[x,y]

proof

let x be Element of Bags n; :: thesis: ex y being Element of F_Real st S₁[x,y]
|.(p . x).| in REAL by XREAL_0:def 1;
hence ex y being Element of F_Real st S₁[x,y] ; :: thesis: verum

end;

consider a being Function of (Bags n), the carrier of F_Real such that
A2: for x being Element of Bags n holds S₁[x,a . x] from FUNCT_2:sch 3(A1);
take a ; :: thesis: for b being bag of n holds a . b = |.(p . b).|
let b be bag of n; :: thesis: a . b = |.(p . b).|
b in Bags n by PRE_POLY:def 12;
hence a . b = |.(p . b).| by A2; :: thesis: verum