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 b1 being Element of F_Real st
for b being OrdBasis of V holds b1 = Det (GramMatrix (f,b)) ; :: thesis: verum