defpred S₁[ object , object ] means for i being Nat st i = $1 holds
$2 = p . (m * i);
A1: for x being object st x in NAT holds
ex y being object st
( y in L & S₁[x,y] )

proof

let x be object ; :: thesis: ( x in NAT implies ex y being object st
( y in L & S₁[x,y] ) )
assume x in NAT ; :: thesis: ex y being object st
( y in L & S₁[x,y] )
then reconsider i = x as Nat ;
take p . (m * i) ; :: thesis: ( p . (m * i) in L & S₁[x,p . (m * i)] )
thus ( p . (m * i) in L & S₁[x,p . (m * i)] ) ; :: thesis: verum

end;

consider f being Function of NAT,L such that
A2: for x being object st x in NAT holds
S₁[x,f . x] from FUNCT_2:sch 1(A1);
take f ; :: thesis: for i being Nat holds f . i = p . (m * i)
thus for i being Nat holds f . i = p . (m * i) by A2, ORDINAL1:def 12; :: thesis: verum