Det (GramMatrix b) <> 0. F_Real by ThGM2;
hence GramMatrix b is invertible by LAPLACE:34; :: thesis: verum