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; :: thesis: verum

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; :: thesis: verum