theorem :: JORDAN2B:19

for s being Real holds abs <*s*> = <*|.s.|*>