let M be non empty multLoopStr ; :: thesis: ( M is well-unital iff for a being Element of M holds
( (1. M) * a = a & a * (1. M) = a ) )
A1: ( M is well-unital iff H₃(M) is_a_unity_wrt H₂(M) ) by Def21;
hence ( M is well-unital implies for a being Element of M holds
( H₃(M) * a = a & a * H₃(M) = a ) ) by BINOP_1:11; :: thesis: ( ( for a being Element of M holds
( (1. M) * a = a & a * (1. M) = a ) ) implies M is well-unital )
assume A2: for a being Element of M holds
( H₃(M) * a = a & a * H₃(M) = a ) ; :: thesis: M is well-unital

now

let a be Element of M; :: thesis: ( H₂(M) . H₃(M),a = a & H₂(M) . a,H₃(M) = a )
( H₃(M) * a = a & a * H₃(M) = a ) by A2;
hence ( H₂(M) . H₃(M),a = a & H₂(M) . a,H₃(M) = a ) ; :: thesis: verum

end;

hence M is well-unital by A1, BINOP_1:11; :: thesis: verum