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