let X be BCI-Algebra_with_Condition(S); :: thesis: the ExternalDiff of X is associative

now

let a, b, c be Element of X; :: thesis: the ExternalDiff of X . a,(the ExternalDiff of X . b,c) = the ExternalDiff of X . (the ExternalDiff of X . a,b),c
thus the ExternalDiff of X . a,(the ExternalDiff of X . b,c) = a * (b * c)
.= (a * b) * c by Th10
.= the ExternalDiff of X . (the ExternalDiff of X . a,b),c ; :: thesis: verum

end;

hence the ExternalDiff of X is associative by BINOP_1:def 3; :: thesis: verum