let A, B, C be complex-membered set ; :: thesis: A /// (B \/ C) = (A /// B) \/ (A /// C)
thus A /// (B \/ C) = A ** ((B "" ) \/ (C "" )) by Th38
.= (A /// B) \/ (A /// C) by Th98 ; :: thesis: verum