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