let X be Banach_Algebra; :: thesis: X is well-unital

let x be Element of X; :: according to VECTSP_1:def 6 :: thesis: ( x * (1. X) = x & (1. X) * x = x )

thus ( x * (1. X) = x & (1. X) * x = x ) by Th38; :: thesis: verum

let x be Element of X; :: according to VECTSP_1:def 6 :: thesis: ( x * (1. X) = x & (1. X) * x = x )

thus ( x * (1. X) = x & (1. X) * x = x ) by Th38; :: thesis: verum