let L be positive-definite Z_Lattice; :: thesis: for b being OrdBasis of L
for e being OrdBasis of EMLat L st e = () * b holds
GramMatrix ((),b) = GramMatrix ((),e)

let b be OrdBasis of L; :: thesis: for e being OrdBasis of EMLat L st e = () * b holds
GramMatrix ((),b) = GramMatrix ((),e)

let e be OrdBasis of EMLat L; :: thesis: ( e = () * b implies GramMatrix ((),b) = GramMatrix ((),e) )
assume AS: e = () * b ; :: thesis: GramMatrix ((),b) = GramMatrix ((),e)
R1: rank L = rank () by ZMODLAT2:42;
R2: ( len (GramMatrix ((),b)) = rank L & width (GramMatrix ((),b)) = rank L & Indices (GramMatrix ((),b)) = [:(Seg (rank L)),(Seg (rank L)):] ) by MATRIX_0:24;
S2: ( len (GramMatrix ((),e)) = rank () & width (GramMatrix ((),e)) = rank () & Indices (GramMatrix ((),e)) = [:(Seg (rank ())),(Seg (rank ())):] ) by MATRIX_0:24;
for i, j being Nat st [i,j] in Indices (GramMatrix ((),b)) holds
(GramMatrix ((),b)) * (i,j) = (GramMatrix ((),e)) * (i,j)
proof
let i, j be Nat; :: thesis: ( [i,j] in Indices (GramMatrix ((),b)) implies (GramMatrix ((),b)) * (i,j) = (GramMatrix ((),e)) * (i,j) )
assume [i,j] in Indices (GramMatrix ((),b)) ; :: thesis: (GramMatrix ((),b)) * (i,j) = (GramMatrix ((),e)) * (i,j)
then X1: ( i in Seg (rank L) & j in Seg (rank L) ) by ;
then A2: ( i in dom b & j in dom b ) by ;
then A3: (GramMatrix ((),b)) * (i,j) = () . ((b /. i),(b /. j)) by ZMODLAT1:def 32;
A4: ( i in dom e & j in dom e ) by ;
Y0: the carrier of () = rng () by ZMODLAT2:def 4
.= the carrier of () by ZMODUL08:def 3 ;
Y1: e /. i = e . i by
.= () . (b . i) by
.= () . (b /. i) by ;
Y2: e /. j = e . j by
.= () . (b . j) by
.= () . (b /. j) by ;
reconsider ei = e /. i, ej = e /. j as Vector of () by Y0;
() . ((e /. i),(e /. j)) = () . (ei,ej) by ZMODLAT2:def 4
.= <;(b /. i),(b /. j);> by
.= () . ((b /. i),(b /. j)) ;
hence (GramMatrix ((),b)) * (i,j) = (GramMatrix ((),e)) * (i,j) by ; :: thesis: verum
end;
hence GramMatrix ((),b) = GramMatrix ((),e) by ; :: thesis: verum