defpred S1[ 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 & S1[x,y] )
proof
let x be
object ;
( x in NAT implies ex y being object st
( y in L & S1[x,y] ) )
assume
x in NAT
;
ex y being object st
( y in L & S1[x,y] )
then reconsider i =
x as
Nat ;
take
p . (m * i)
;
( p . (m * i) in L & S1[x,p . (m * i)] )
thus
(
p . (m * i) in L &
S1[
x,
p . (m * i)] )
;
verum
end;
consider f being Function of NAT,L such that
A2:
for x being object st x in NAT holds
S1[x,f . x]
from FUNCT_2:sch 1(A1);
take
f
; 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; verum