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 ThSc5
.= (<;v,v;> - <;v,u;>) - <;u,(v - u);> by ThSc5
.= (<;v,v;> - 0) - (<;u,v;> - <;u,u;>) by A1, ThSc5
.= <;v,v;> - (0 - <;u,u;>) by A1, defZLattice
.= ||.v.|| + ||.u.|| ; :: thesis: verum