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

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