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