Does it negatively affect security to calculate a hash value of the ciphertext before MAC calculation? Like exchanging step 2. with this: HMAC-SHA256(SHA256(ciphertext)).
Technically, yes, but not significantly. In order to attack the scheme you propose, the attacker would have to be able to do at least one of two things: (1) Find an attack on the (standard) HMAC-SHA256 scheme; or (2) Find a collision for SHA256. Currently, the cryptographic community believes that one can safely assume an attacker can do neither of these things. (Contrary to what some may expect, an ability to do the second does not imply an ability to do the first.)
What security properties are offered by this construction in general -- because I don't understand, what about this construction is provably secure.
What do you mean by "this construction"? Do you mean Encrypt-then-Mac, or HMAC-SHA256?
If you meant Encrypt-then-MAC, David Cary provided a link to this question, and you might find the answers helpful. To summarize, one can prove that an attacker cannot learn information about the plaintexts (aside from their lengths), and cannot create a ciphertext that will pass the MAC integrity check. Here, attackers are assumed to have the ability to conduct chosen message attacks; that is, we assume that the attacker can convince or trick one of the parties into sending some messages of the attacker's choosing, and show that having this power is not enough for the attacker to "break" the scheme. (This is very conservative: in the real world, most attackers won't have this ability.) We also assume that the encryption algorithm and the MAC algorithm are themselves secure, and use independently chosen, random keys.
If you meant HMAC-SHA256, then see the second part of my answer to another question. Proving that HMAC-SHA256 has the properties discussed there requires making some (reasonable) assumptions about SHA256.
In both cases, the proofs are not "absolute". We need to make assumptions about the underlying algorithms, and the proof only shows that the probability of the attacker succeeding is very small, provided you don't do something like use the same key to encrypt petabytes of data.
In your question, you wrote
Ciphertext = AES_K(Plaintext). But this is (almost always) wrong! AES can only work on 16-byte strings. To encrypt longer strings, you need to use AES inside of some mode of operation.