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