let x, y, z be Element of [:S,T:]; :: according to WAYBEL_1:def 3 :: thesis: x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z)
A1: the carrier of [:S,T:] = [: the carrier of S, the carrier of T:] by YELLOW_3:def 2;
A2: (x "/\" (y "\/" z)) `2 = (x `2) "/\" ((y "\/" z) `2) by Th13
.= (x `2) "/\" ((y `2) "\/" (z `2)) by Th14
.= ((x `2) "/\" (y `2)) "\/" ((x `2) "/\" (z `2)) by WAYBEL_1:def 3
.= ((x "/\" y) `2) "\/" ((x `2) "/\" (z `2)) by Th13
.= ((x "/\" y) `2) "\/" ((x "/\" z) `2) by Th13
.= ((x "/\" y) "\/" (x "/\" z)) `2 by Th14 ;
(x "/\" (y "\/" z)) `1 = (x `1) "/\" ((y "\/" z) `1) by Th13
.= (x `1) "/\" ((y `1) "\/" (z `1)) by Th14
.= ((x `1) "/\" (y `1)) "\/" ((x `1) "/\" (z `1)) by WAYBEL_1:def 3
.= ((x "/\" y) `1) "\/" ((x `1) "/\" (z `1)) by Th13
.= ((x "/\" y) `1) "\/" ((x "/\" z) `1) by Th13
.= ((x "/\" y) "\/" (x "/\" z)) `1 by Th14 ;
hence x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z) by A1, A2, DOMAIN_1:2; :: thesis: verum