let X be Banach_Algebra; :: thesis: for z being Element of X holds
( exp z is invertible & (exp z) " = exp (- z) & exp (- z) is invertible & (exp (- z)) " = exp z )
let z be Element of X; :: thesis: ( exp z is invertible & (exp z) " = exp (- z) & exp (- z) is invertible & (exp (- z)) " = exp z )
A1: (exp (- z)) * (exp z) = 1. X by Th38;
A2: (exp z) * (exp (- z)) = 1. X by Th38;
hence exp z is invertible by A1; :: thesis: ( (exp z) " = exp (- z) & exp (- z) is invertible & (exp (- z)) " = exp z )
hence (exp z) " = exp (- z) by A2, A1, LOPBAN_3:def 8; :: thesis: ( exp (- z) is invertible & (exp (- z)) " = exp z )
thus exp (- z) is invertible by A2, A1; :: thesis: (exp (- z)) " = exp z
hence (exp (- z)) " = exp z by A2, A1, LOPBAN_3:def 8; :: thesis: verum