theorem :: ZMODLAT1:19

for L being Z_Lattice
for v, u being Vector of L st v,u are_orthogonal holds
||.(v + u).|| = ||.v.|| + ||.u.||