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

now :: thesis: for a being Element of X holds
( the ExternalDiff of X . ((0. X),a) = a & the ExternalDiff of X . (a,(0. X)) = a )

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 Th8 ; :: thesis: the ExternalDiff of X . (a,(0. X)) = a
thus the ExternalDiff of X . (a,(0. X)) = a * (0. X)
.= a by Th8 ; :: thesis: verum

end;

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