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

proof

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
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;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