set r = <*> [:{},{}:];
dom (pr1 (<*> [:{},{}:])) = dom {} by MCART_1:def 12
.= {} ;
hence pr1 {} = {} ; :: thesis: pr2 {} = {}
dom (pr2 (<*> [:{},{}:])) = dom {} by MCART_1:def 13
.= {} ;
hence pr2 {} = {} ; :: thesis: verum