for a, b being Real holds
( |[a,b]| . 1 = a & |[a,b]| . 2 = b )