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

proof

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

end;

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