let a, b, c, d be Complex; :: thesis: Product <*a,b,c,d*> = ((a * b) * c) * d
thus Product <*a,b,c,d*> = (Product <*a,b,c*>) * d by RVSUM_1:96
.= ((a * b) * c) * d by RVSUM_1:100 ; :: thesis: verum