take RN_Base n ; :: thesis: RN_Base n is orthogonal_basis
thus RN_Base n is orthogonal_basis ; :: thesis: verum