defpred S₁[ object , object ] means ex n being positive Nat st
( n = $1 & $2 = n (#) f );
A1: for i being object st i in NATPLUS holds
ex j being object st S₁[i,j]

proof

let i be object ; :: thesis: ( i in NATPLUS implies ex j being object st S₁[i,j] )
assume i in NATPLUS ; :: thesis: ex j being object st S₁[i,j]
then reconsider i = i as non zero Nat ;
take i (#) f ; :: thesis: S₁[i,i (#) f]
thus S₁[i,i (#) f] ; :: thesis: verum

end;

consider F being ManySortedSet of NATPLUS such that
A2: for i being object st i in NATPLUS holds
S₁[i,F . i] from PBOOLE:sch 3(A1);
take F ; :: thesis: for n being non zero Nat holds F . n = n (#) f
let n be non zero Nat; :: thesis: F . n = n (#) f
n in NATPLUS by NAT_LAT:def 6;
then S₁[n,F . n] by A2;
hence F . n = n (#) f ; :: thesis: verum