let X be BCI-Algebra_with_Condition(S); :: thesis: 0. X is_a_unity_wrt the ExternalDiff of X

now

let a be Element of X; :: thesis: ( the ExternalDiff of X . (0. X),a = a & the ExternalDiff of X . a,(0. X) = a )
thus the ExternalDiff of X . (0. X),a = (0. X) * a
.= a by Th9 ; :: thesis: the ExternalDiff of X . a,(0. X) = a
thus the ExternalDiff of X . a,(0. X) = a * (0. X)
.= a by Th9 ; :: thesis: verum

end;

hence 0. X is_a_unity_wrt the ExternalDiff of X by BINOP_1:11; :: thesis: verum