theorem :: TOPREAL6:13

for a, b being Real holds abs <*a,b*> = <*|.a.|,|.b.|*>