defpred S₁[ bag of m, object ] means $2 = P . ((2 (#) $1) +* (0,($1 . 0)));
A1: for x being Element of Bags m ex y being Element of L st S₁[x,y] ;
consider P being Function of (Bags m), the carrier of L such that
A2: for b being Element of Bags m holds S₁[b,P . b] from FUNCT_2:sch 3(A1);
take P ; :: thesis: for b being bag of m holds P . b = P . ((2 (#) b) +* (0,(b . 0)))
let b be bag of m; :: thesis: P . b = P . ((2 (#) b) +* (0,(b . 0)))
b in Bags m by PRE_POLY:def 12;
hence P . b = P . ((2 (#) b) +* (0,(b . 0))) by A2; :: thesis: verum