let X be BCI-Algebra_with_Condition(S); :: thesis: the ExternalDiff of X is having_a_unity

reconsider e = 0. X as Element of X ;

e is_a_unity_wrt the ExternalDiff of X by Th16;

hence the ExternalDiff of X is having_a_unity by SETWISEO:def 2; :: thesis: verum

reconsider e = 0. X as Element of X ;

e is_a_unity_wrt the ExternalDiff of X by Th16;

hence the ExternalDiff of X is having_a_unity by SETWISEO:def 2; :: thesis: verum