let L be Z_Lattice; :: thesis: for b being OrdBasis of L st GramMatrix ((InnerProduct L),b) is Matrix of dim L,F_Rat holds
L is RATional
let b be OrdBasis of L; :: thesis: ( GramMatrix ((InnerProduct L),b) is Matrix of dim L,F_Rat implies L is RATional )
assume A1: GramMatrix ((InnerProduct L),b) is Matrix of dim L,F_Rat ; :: thesis: L is RATional
set I = rng b;
reconsider I = rng b as Basis of L by ZMATRLIN:def 5;
set GM = GramMatrix ((InnerProduct L),b);
reconsider GMR = GramMatrix ((InnerProduct L),b) as Matrix of dim L,F_Rat by A1;
for v, u being Vector of L st v in I & u in I holds
<;v,u;> in RAT

proof

let v, u be Vector of L; :: thesis: ( v in I & u in I implies <;v,u;> in RAT )
assume B1: ( v in I & u in I ) ; :: thesis: <;v,u;> in RAT
consider i being Nat such that
B2: ( i in dom b & b . i = v ) by B1, FINSEQ_2:10;
consider j being Nat such that
B3: ( j in dom b & b . j = u ) by B1, FINSEQ_2:10;
B4: b /. i = v by B2, PARTFUN1:def 6;
B6: (GramMatrix ((InnerProduct L),b)) * (i,j) = (InnerProduct L) . ((b /. i),(b /. j)) by B2, B3, ZMODLAT1:def 32
.= <;v,u;> by B3, B4, PARTFUN1:def 6 ;
B7: dom b = Seg (len b) by FINSEQ_1:def 3
.= Seg (dim L) by ZMATRLIN:49 ;
Indices (GramMatrix ((InnerProduct L),b)) = [:(Seg (dim L)),(Seg (dim L)):] by MATRIX_0:24;
then [i,j] in Indices (GramMatrix ((InnerProduct L),b)) by B2, B3, B7, ZFMISC_1:87;
then (GramMatrix ((InnerProduct L),b)) * (i,j) = GMR * (i,j) by ZMATRLIN:1;
hence <;v,u;> in RAT by B6; :: thesis: verum

end;

hence L is RATional by ThRatLat1; :: thesis: verum