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