( 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 i' = i as Element of NAT by INT_1:16;
(power L) . a,i' 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,(abs i)) " is Element of L ) ) ; :: thesis: verum