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 )

proof

given e being Element of IT such that A1: for h being Element of IT holds
( h * e = h & e * h = h ) ; :: according to GROUP_1:def 2 :: thesis: the multF of IT is having_a_unity
take e ; :: according to SETWISEO:def 2 :: thesis: e is_a_unity_wrt the multF of IT
for a being Element of IT holds
( the multF of IT . e,a = a & the multF of IT . a,e = a )

proof

let a be Element of IT; :: thesis: ( the multF of IT . e,a = a & the multF of IT . a,e = a )
thus the multF of IT . e,a = e * a
.= a by A1 ; :: thesis: the multF of IT . a,e = a
thus the multF of IT . a,e = a * e
.= a by A1 ; :: thesis: verum

end;

hence e is_a_unity_wrt the multF of IT by BINOP_1:11; :: thesis: verum

end;

given x being Element of IT such that A2: 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 2 :: 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 A2, BINOP_1:11; :: thesis: verum