The KeY System 1.0 (Deduction Component) Bernhard Beckert, Martin Giese, Reiner H\"ahnle, Vladimir Klebanov, Philipp R\"ummer, Steffen Schlager, and Peter H. Schmitt The KeY system is a development of the ongoing KeY project, whose aim is to integrate formal specification and deductive verification into the industrial software engineering processes. The deductive component of the KeY system is a novel interactive/automated prover for first-order Dynamic Logic for Java. The KeY prover features a user-friendly graphical interface, a backtracking-free free-variable sequent calculus with equality, a simple and powerful theory formalization language called "taclets," solution procedures for linear and non-linear integer arithmetic, external theorem prover integration, and facilities for proof reuse, among other aspects. The system is publicly available.