let a, b be Point of E; :: according to MAZURULM:def 1 :: thesis: ||.(((id E) . a) - ((id E) . b)).|| = ||.(a - b).||
( (id E) . a = a & (id E) . b = b ) by FUNCT_1:18;
hence ||.(((id E) . a) - ((id E) . b)).|| = ||.(a - b).|| ; :: thesis: verum