:: deftheorem defines *' MIDSP_3:def 1 :
for n being Nat
for RAS being non empty MidSp-like ReperAlgebraStr over n + 2
for a being Point of RAS
for p being Tuple of (n + 1),RAS holds *' (a,p) = the reper of RAS . (<*a*> ^ p);