let L be INTegral Z_Lattice; :: thesis: for b being OrdBasis of L holds GramMatrix b is Matrix of dim L,INT.Ring
let b be OrdBasis of L; :: thesis: GramMatrix b is Matrix of dim L,INT.Ring
X1: ( len (GramMatrix b) = dim L & width (GramMatrix b) = dim L & Indices (GramMatrix b) = [:(Seg (dim L)),(Seg (dim L)):] ) by MATRIX_0:24;
X3: len b = dim L by ZMATRLIN:49;
for i, j being Nat st [i,j] in Indices (GramMatrix b) holds
(GramMatrix b) * (i,j) in the carrier of INT.Ring

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices (GramMatrix b) implies (GramMatrix b) * (i,j) in the carrier of INT.Ring )
assume [i,j] in Indices (GramMatrix b) ; :: thesis: (GramMatrix b) * (i,j) in the carrier of INT.Ring
then ( i in Seg (dim L) & j in Seg (dim L) ) by X1, ZFMISC_1:87;
then D1: ( i in dom b & j in dom b ) by X3, FINSEQ_1:def 3;
(GramMatrix b) * (i,j) = (InnerProduct L) . ((b /. i),(b /. j)) by defBilinearM, D1
.= <;(b /. i),(b /. j);> ;
hence (GramMatrix b) * (i,j) in the carrier of INT.Ring by defIntegral; :: thesis: verum

end;

hence GramMatrix b is Matrix of dim L,INT.Ring by LMEQ; :: thesis: verum