defpred S₁[ Element of (D *) \ {{}}, Element of D] means $2 = (MultPlace (f,$1)) . ((len $1) - 1);
A1: for x being Element of (D *) \ {{}} ex y being Element of D st S₁[x,y]

proof

let x be Element of (D *) \ {{}}; :: thesis: ex y being Element of D st S₁[x,y]
reconsider x1 = x as Element of D * ;
not x1 in {{}} by XBOOLE_0:def 5;
then x1 <> {} by TARSKI:def 1;
then len x1 >= 1 by FINSEQ_1:20;
then (len x1) - 1 in NAT by INT_1:3, XREAL_1:48;
then reconsider m = (len x1) - 1 as Nat ;
A2: m + 1 <= len x1 ;
reconsider y = (MultPlace (f,x1)) . m as Element of D by Lm14, A2;
take y ; :: thesis: S₁[x,y]
thus S₁[x,y] ; :: thesis: verum

end;

consider g being Function of ((D *) \ {{}}),D such that
A3: for x being Element of (D *) \ {{}} holds S₁[x,g . x] from FUNCT_2:sch 3(A1);
take g ; :: thesis: for x being Element of (D *) \ {{}} holds g . x = (MultPlace (f,x)) . ((len x) - 1)
thus for x being Element of (D *) \ {{}} holds g . x = (MultPlace (f,x)) . ((len x) - 1) by A3; :: thesis: verum