theorem :: ZMODLAT2:44

for L being RATional Z_Lattice
for v, u being Vector of (DivisibleMod L) holds (ScProductDM L) . (v,u) in F_Rat by RAT_1:def 2;