set p = <*> the carrier of R;
take <*> the carrier of R ; :: thesis: for i being set st i in dom (<*> the carrier of R) holds
ex u, v being Element of R ex a being Element of A st (<*> the carrier of R) /. i = (u * a) * v
let i be set ; :: thesis: ( i in dom (<*> the carrier of R) implies ex u, v being Element of R ex a being Element of A st (<*> the carrier of R) /. i = (u * a) * v )
assume i in dom (<*> the carrier of R) ; :: thesis: ex u, v being Element of R ex a being Element of A st (<*> the carrier of R) /. i = (u * a) * v
hence ex u, v being Element of R ex a being Element of A st (<*> the carrier of R) /. i = (u * a) * v ; :: thesis: verum