defpred S_{1}[ object , object ] means $2 = |.(p . $1).|;

A1: for x being Element of Bags n ex y being Element of F_Real st S_{1}[x,y]

A2: for x being Element of Bags n holds S_{1}[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

A1: for x being Element of Bags n ex y being Element of F_Real st S

proof

consider a being Function of (Bags n), the carrier of F_Real such that
let x be Element of Bags n; :: thesis: ex y being Element of F_Real st S_{1}[x,y]

|.(p . x).| in REAL by XREAL_0:def 1;

hence ex y being Element of F_Real st S_{1}[x,y]
; :: thesis: verum

end;|.(p . x).| in REAL by XREAL_0:def 1;

hence ex y being Element of F_Real st S

A2: for x being Element of Bags n holds S

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