let X be Complex_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 Th37;

A2: (exp z) * (exp (- z)) = 1. X by Th37;

hence exp z is invertible by A1, LOPBAN_3:def 4; :: 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, LOPBAN_3:def 4; :: thesis: (exp (- z)) " = exp z

hence (exp (- z)) " = exp z by A2, A1, LOPBAN_3:def 8; :: thesis: verum

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

A2: (exp z) * (exp (- z)) = 1. X by Th37;

hence exp z is invertible by A1, LOPBAN_3:def 4; :: 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, LOPBAN_3:def 4; :: thesis: (exp (- z)) " = exp z

hence (exp (- z)) " = exp z by A2, A1, LOPBAN_3:def 8; :: thesis: verum