theorem :: RFINSEQ:14

for r, s being Real holds MIM <*r,s*> = <*(r - s),s*>