let L be non trivial positive-definite RATional Z_Lattice; :: thesis: for b being OrdBasis of L ex a being Element of F_Real st
( a is Element of INT.Ring & a <> 0 & a * (() ~) is Matrix of dim L,INT.Ring )

let b be OrdBasis of L; :: thesis: ex a being Element of F_Real st
( a is Element of INT.Ring & a <> 0 & a * (() ~) is Matrix of dim L,INT.Ring )

set G = () ~ ;
reconsider M = () ~ as Matrix of dim L,F_Rat by ThGM3;
A2: rng M c= the carrier of F_Rat * ;
A5: ( len M = dim L & width M = dim L ) by MATRIX_0:24;
B1: for i, j being Nat st [i,j] in Indices (() ~) holds
(() ~) * (i,j) in the carrier of F_Rat
proof
let i, j be Nat; :: thesis: ( [i,j] in Indices (() ~) implies (() ~) * (i,j) in the carrier of F_Rat )
assume B10: [i,j] in Indices (() ~) ; :: thesis: (() ~) * (i,j) in the carrier of F_Rat
then consider p being FinSequence of F_Real such that
B11: ( p = (() ~) . i & (() ~) * (i,j) = p . j ) by MATRIX_0:def 5;
B12: ( i in dom (() ~) & j in Seg (width (() ~)) ) by ;
then p in rng (() ~) by ;
then B14: len p = width (() ~) by ;
p in the carrier of F_Rat * by ;
then p is FinSequence of F_Rat by FINSEQ_1:def 11;
then B15: rng p c= the carrier of F_Rat by FINSEQ_1:def 4;
j in dom p by ;
hence ((GramMatrix b) ~) * (i,j) in the carrier of F_Rat by ; :: thesis: verum
end;
deffunc H1( Nat, Nat) -> Element of the carrier of F_Real = (() ~) * (\$1,\$2);
set Dn = { H1(u,v) where u, v is Element of NAT : ( u in Seg (len (() ~)) & v in Seg (width (() ~)) ) } ;
F1: Seg (len (() ~)) is finite ;
F2: Seg (width (() ~)) is finite ;
F3: { H1(u,v) where u, v is Element of NAT : ( u in Seg (len (() ~)) & v in Seg (width (() ~)) ) } is finite from D2: { (((GramMatrix b) ~) * (i,j)) where i, j is Nat : [i,j] in Indices (() ~) } c= { H1(u,v) where u, v is Element of NAT : ( u in Seg (len (() ~)) & v in Seg (width (() ~)) ) }
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { ((() ~) * (i,j)) where i, j is Nat : [i,j] in Indices (() ~) } or x in { H1(u,v) where u, v is Element of NAT : ( u in Seg (len (() ~)) & v in Seg (width (() ~)) ) } )
assume x in { ((() ~) * (i,j)) where i, j is Nat : [i,j] in Indices (() ~) } ; :: thesis: x in { H1(u,v) where u, v is Element of NAT : ( u in Seg (len (() ~)) & v in Seg (width (() ~)) ) }
then consider i, j being Nat such that
F40: ( x = (() ~) * (i,j) & [i,j] in Indices (() ~) ) ;
( i in dom (() ~) & j in Seg (width (() ~)) ) by ;
then ( i in Seg (len (() ~)) & j in Seg (width (() ~)) ) by FINSEQ_1:def 3;
hence x in { H1(u,v) where u, v is Element of NAT : ( u in Seg (len (() ~)) & v in Seg (width (() ~)) ) } by F40; :: thesis: verum
end;
{ (((GramMatrix b) ~) * (i,j)) where i, j is Nat : [i,j] in Indices (() ~) } c= the carrier of F_Rat
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { ((() ~) * (i,j)) where i, j is Nat : [i,j] in Indices (() ~) } or x in the carrier of F_Rat )
assume x in { ((() ~) * (i,j)) where i, j is Nat : [i,j] in Indices (() ~) } ; :: thesis: x in the carrier of F_Rat
then consider i, j being Nat such that
D1: ( x = (() ~) * (i,j) & [i,j] in Indices (() ~) ) ;
thus x in the carrier of F_Rat by B1, D1; :: thesis: verum
end;
then reconsider X = { ((() ~) * (i,j)) where i, j is Nat : [i,j] in Indices (() ~) } as finite Subset of F_Rat by D2, F3;
consider a being Element of INT such that
A10: ( a <> 0 & ( for r being Element of RAT st r in X holds
a * r in INT ) ) by LmDE311A;
reconsider a = a as Element of F_Real by NUMBERS:15;
A6: ( len (a * (() ~)) = dim L & width (a * (() ~)) = dim L ) by MATRIX_0:24;
take a ; :: thesis: ( a is Element of INT.Ring & a <> 0 & a * (() ~) is Matrix of dim L,INT.Ring )
thus ( a is Element of INT.Ring & a <> 0 ) by A10; :: thesis: a * (() ~) is Matrix of dim L,INT.Ring
for i, j being Nat st [i,j] in Indices (a * (() ~)) holds
(a * (() ~)) * (i,j) in the carrier of INT.Ring
proof
let i, j be Nat; :: thesis: ( [i,j] in Indices (a * (() ~)) implies (a * (() ~)) * (i,j) in the carrier of INT.Ring )
assume B1: [i,j] in Indices (a * (() ~)) ; :: thesis: (a * (() ~)) * (i,j) in the carrier of INT.Ring
B2: Indices (() ~) = [:(Seg (dim L)),(Seg (dim L)):] by MATRIX_0:24
.= Indices (a * (() ~)) by MATRIX_0:24 ;
then B3: (a * (() ~)) * (i,j) = a * ((() ~) * (i,j)) by ;
((GramMatrix b) ~) * (i,j) in X by B1, B2;
hence (a * (() ~)) * (i,j) in the carrier of INT.Ring by ; :: thesis: verum
end;
hence a * (() ~) is Matrix of dim L,INT.Ring by ; :: thesis: verum