let L be Z_Lattice; :: thesis: for b being OrdBasis of L st GramMatrix ((),b) is Matrix of dim L,F_Rat holds
L is RATional

let b be OrdBasis of L; :: thesis: ( GramMatrix ((),b) is Matrix of dim L,F_Rat implies L is RATional )
assume A1: GramMatrix ((),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 ((),b);
reconsider GMR = GramMatrix ((),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 ;
consider j being Nat such that
B3: ( j in dom b & b . j = u ) by ;
B4: b /. i = v by ;
B6: (GramMatrix ((),b)) * (i,j) = () . ((b /. i),(b /. j)) by
.= <;v,u;> by ;
B7: dom b = Seg (len b) by FINSEQ_1:def 3
.= Seg (dim L) by ZMATRLIN:49 ;
Indices (GramMatrix ((),b)) = [:(Seg (dim L)),(Seg (dim L)):] by MATRIX_0:24;
then [i,j] in Indices (GramMatrix ((),b)) by ;
then (GramMatrix ((),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