let L be Z_Lattice; :: thesis: for v, u being Vector of L st v,u are_orthogonal holds
||.(v + u).|| = ||.v.|| + ||.u.||
let v, u be Vector of L; :: thesis: ( v,u are_orthogonal implies ||.(v + u).|| = ||.v.|| + ||.u.|| )
assume A1: v,u are_orthogonal ; :: thesis: ||.(v + u).|| = ||.v.|| + ||.u.||
thus ||.(v + u).|| = <;v,(v + u);> + <;u,(v + u);> by defZLattice
.= (<;v,v;> + <;v,u;>) + <;u,(v + u);> by ThSc2
.= (<;v,v;> + 0) + (<;u,v;> + <;u,u;>) by A1, ThSc2
.= <;v,v;> + (0 + <;u,u;>) by A1, defZLattice
.= ||.v.|| + ||.u.|| ; :: thesis: verum