thus ( IT is unital implies the multF of IT is having_a_unity ) ; :: thesis: ( the multF of IT is having_a_unity implies IT is unital )
given x being Element of IT such that A1: x is_a_unity_wrt the multF of IT ; :: according to SETWISEO:def 2 :: thesis: IT is unital
take x ; :: according to GROUP_1:def 1 :: thesis: for b₁ being Element of the carrier of IT holds
( b₁ [*] x = b₁ & x [*] b₁ = b₁ )
let h be Element of IT; :: thesis: ( h [*] x = h & x [*] h = h )
thus ( h [*] x = h & x [*] h = h ) by A1, BINOP_1:3; :: thesis: verum