defpred S₁[ 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 & S₁[x,y] )

let x be object ; :: thesis: ( x in NAT implies ex y being object st
( y in the carrier of L & S₁[x,y] ) )
assume A13: x in NAT ; :: thesis: ex y being object st
( y in the carrier of L & S₁[x,y] )
thus ex y being object st
( y in the carrier of L & S₁[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 & S₁[x,y] )

take 0. L ; :: thesis: ( 0. L in the carrier of L & S₁[x, 0. L] )
thus ( 0. L in the carrier of L & S₁[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 & S₁[x,y] )

take p . m ; :: thesis: ( p . m in the carrier of L & S₁[x,p . m] )
thus ( p . m in the carrier of L & S₁[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
S₁[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 ) )

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