defpred S_{1}[ object , object ] means for i being Nat st i = $1 holds

( ( i is even implies $2 = 0. L ) & ( i is odd implies $2 = p . $1 ) );

A16: for x being object st x in NAT holds

S_{1}[x,f . x]
from FUNCT_2:sch 1(A12);

take f ; :: thesis: for i being even Nat holds

( f . i = 0. L & ( for i being odd Nat holds f . i = p . i ) )

( f . i = 0. L & ( for i being odd Nat holds f . i = p . i ) ) by A17; :: thesis: verum

( ( i is even implies $2 = 0. L ) & ( i is odd implies $2 = p . $1 ) );

A12: now :: thesis: for x being object st x in NAT holds

ex y being object st

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

consider f being Function of NAT, the carrier of L such that ex y being object st

( y in the carrier of L & S

let x be object ; :: thesis: ( x in NAT implies ex y being object st

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

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

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

thus ex y being object st

( y in the carrier of L & S_{1}[x,y] )
:: thesis: verum

end;( y in the carrier of L & S

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

( y in the carrier of L & S

thus ex y being object st

( y in the carrier of L & S

proof

reconsider m = x as Nat by A13;

end;A16: for x being object st x in NAT holds

S

take f ; :: thesis: for i being even Nat holds

( f . i = 0. L & ( for i being odd Nat holds f . i = p . i ) )

A17: now :: thesis: for i being even Nat holds f . i = 0. L

let i be even Nat; :: thesis: f . i = 0. L

i is Element of NAT by ORDINAL1:def 12;

hence f . i = 0. L by A16; :: thesis: verum

end;i is Element of NAT by ORDINAL1:def 12;

hence f . i = 0. L by A16; :: thesis: verum

now :: thesis: for i being odd Nat holds f . i = p . i

hence
for i being even Nat holds let i be odd Nat; :: thesis: f . i = p . i

i is Element of NAT by ORDINAL1:def 12;

hence f . i = p . i by A16; :: thesis: verum

end;i is Element of NAT by ORDINAL1:def 12;

hence f . i = p . i by A16; :: thesis: verum

( f . i = 0. L & ( for i being odd Nat holds f . i = p . i ) ) by A17; :: thesis: verum