Embedding Henselian fields into power series

Every Henselian field of residue characteristic 0 admits a truncation-closed embedding in a field of generalised power series (possibly, with a factor set). As corollaries we obtain the Ax–Kochen–Ershov theorem and an extension of Mourgues and Ressayre's theorem: every ordered field which is Henselian in its natural valuation has an integer part. We also give some results for the mixed and the finite characteristic cases.