consider i being Element of INT.Ring such that
A1:
( i <> 0 & i * v in EMbedding L )
by ZMODUL08:29;
consider j being Element of INT.Ring such that
A2:
( j <> 0 & j * u in EMbedding L )
by ZMODUL08:29;
reconsider iv = i * v, ju = j * u as Vector of (EMbedding L) by A1, A2;
reconsider a = i, b = j as Element of INT ;
reconsider a = a, b = b as Element of F_Real by XREAL_0:def 1;
A3:
(ScProductDM L) . (v,u) = ((a ") * (b ")) * ((ScProductEM L) . (iv,ju))
by A1, A2, defScProductDM;
A4:
( iv is Vector of (EMLat L) & ju is Vector of (EMLat L) )
by ThEME1;
reconsider ar = a, br = b as Element of F_Rat by RAT_1:def 2;
( a <> 0. F_Real & b <> 0. F_Real )
by A1, A2;
then
( a " = ar " & b " = br " )
by GAUSSINT:14, GAUSSINT:21;
hence
(ScProductDM L) . (v,u) is rational
by A3, A4; verum