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:12; :: thesis: verum