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 )

hence
0. X is_a_unity_wrt the ExternalDiff of X
by BINOP_1:3; :: thesis: verum( 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;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