let X be RealNormSpace; :: thesis: for x, y, z being Element of X holds ||.(x - y).|| = ||.((x - z) + (z - y)).||
let x, y, z be Element of X; :: thesis: ||.(x - y).|| = ||.((x - z) + (z - y)).||
thus ||.(x - y).|| = ||.((x - (0. X)) - y).|| by RLVECT_1:13
.= ||.((x - (z - z)) - y).|| by RLVECT_1:5
.= ||.(((x - z) + z) - y).|| by RLVECT_1:29
.= ||.((x - z) + (z - y)).|| by RLVECT_1:def 3 ; :: thesis: verum