(<*(a "),b*> ") . 1 = (<*(a "),b*> . 1) " by VALUED_1:10;
hence (<*(a "),b*> ") . 1 = a ; :: thesis: verum