( 0 <= i implies (power L) . (a,i) is Element of L )

proof

assume 0 <= i ; :: thesis: (power L) . (a,i) is Element of L
then reconsider i9 = i as Element of NAT by INT_1:3;
(power L) . (a,i9) is Element of L ;
hence (power L) . (a,i) is Element of L ; :: thesis: verum

end;

hence ( ( 0 <= i implies (power L) . (a,i) is Element of L ) & ( not 0 <= i implies ((power L) . (a,|.i.|)) " is Element of L ) ) ; :: thesis: verum