defpred S1[ 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 ) );
A12: now :: thesis: for x being object st x in NAT holds
ex y being object st
( y in the carrier of L & S1[x,y] )
let x be object ; :: thesis: ( x in NAT implies ex y being object st
( y in the carrier of L & S1[x,y] ) )

assume A13: x in NAT ; :: thesis: ex y being object st
( y in the carrier of L & S1[x,y] )

thus ex y being object st
( y in the carrier of L & S1[x,y] ) :: thesis: verum
proof
reconsider m = x as Nat by A13;
per cases ( m is even or m is odd ) ;
suppose A14: m is even ; :: thesis: ex y being object st
( y in the carrier of L & S1[x,y] )

take 0. L ; :: thesis: ( 0. L in the carrier of L & S1[x, 0. L] )
thus ( 0. L in the carrier of L & S1[x, 0. L] ) by A14; :: thesis: verum
end;
suppose A15: m is odd ; :: thesis: ex y being object st
( y in the carrier of L & S1[x,y] )

take p . m ; :: thesis: ( p . m in the carrier of L & S1[x,p . m] )
thus ( p . m in the carrier of L & S1[x,p . m] ) by A15; :: thesis: verum
end;
end;
end;
end;
consider f being Function of NAT, the carrier of L such that
A16: for x being object st x in NAT holds
S1[x,f . x] from 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;
now :: thesis: for i being odd Nat holds f . i = p . i
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;
hence for i being even Nat holds
( f . i = 0. L & ( for i being odd Nat holds f . i = p . i ) ) by A17; :: thesis: verum