defpred S_{1}[ 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_{1}[x,y] )

A2: for x being object st x in NAT holds

S_{1}[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

$2 = p . (m * i);

A1: for x being object st x in NAT holds

ex y being object st

( y in L & S

proof

consider f being Function of NAT,L such that
let x be object ; :: thesis: ( x in NAT implies ex y being object st

( y in L & S_{1}[x,y] ) )

assume x in NAT ; :: thesis: ex y being object st

( y in L & S_{1}[x,y] )

then reconsider i = x as Nat ;

take p . (m * i) ; :: thesis: ( p . (m * i) in L & S_{1}[x,p . (m * i)] )

thus ( p . (m * i) in L & S_{1}[x,p . (m * i)] )
; :: thesis: verum

end;( y in L & S

assume x in NAT ; :: thesis: ex y being object st

( y in L & S

then reconsider i = x as Nat ;

take p . (m * i) ; :: thesis: ( p . (m * i) in L & S

thus ( p . (m * i) in L & S

A2: for x being object st x in NAT holds

S

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