let X be BCI-Algebra_with_Condition(S); :: thesis: the_unity_wrt the ExternalDiff of X = 0. X
reconsider e = 0. X as Element of X ;
e is_a_unity_wrt the ExternalDiff of X by Th16;
hence the_unity_wrt the ExternalDiff of X = 0. X by BINOP_1:def 8; :: thesis: verum