reconsider p9 = <*a*> ^ p as Tuple of (n + 2),RAS ;
the reper of RAS . p9 is Point of RAS ;
hence the reper of RAS . (<*a*> ^ p) is Point of RAS ; :: thesis: verum