defpred S1[ object , object ] means $2 = |.(p . $1).|;
A1: for x being Element of Bags n ex y being Element of F_Real st S1[x,y]
proof
let x be Element of Bags n; :: thesis: ex y being Element of F_Real st S1[x,y]
|.(p . x).| in REAL by XREAL_0:def 1;
hence ex y being Element of F_Real st S1[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 S1[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