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

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

hence
the ExternalDiff of X is associative
; :: thesis: verumlet 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 Th9

.= the ExternalDiff of X . (( the ExternalDiff of X . (a,b)),c) ; :: thesis: verum

end;thus the ExternalDiff of X . (a,( the ExternalDiff of X . (b,c))) = a * (b * c)

.= (a * b) * c by Th9

.= the ExternalDiff of X . (( the ExternalDiff of X . (a,b)),c) ; :: thesis: verum