set b1 = the OrdBasis of V;
for b being OrdBasis of V holds Det (GramMatrix (f,b)) = Det (GramMatrix (f, the OrdBasis of V))

proof

let b be OrdBasis of V; :: thesis: Det (GramMatrix (f,b)) = Det (GramMatrix (f, the OrdBasis of V))
thus Det (GramMatrix (f,b)) = Det (BilinearM (f,b,b)) by ZMATRLIN:49
.= Det (BilinearM (f, the OrdBasis of V, the OrdBasis of V)) by ThMBFY
.= Det (GramMatrix (f, the OrdBasis of V)) by ZMATRLIN:49 ; :: thesis: verum

end;

hence ex b₁ being Element of F_Real st
for b being OrdBasis of V holds b₁ = Det (GramMatrix (f,b)) ; :: thesis: verum