A1:
v is Vector of (EMbedding L)
by ThEME1;

then consider vv being Vector of L such that

A2: (MorphsZQ L) . vv = v by ZMODUL08:22;

A3: u is Vector of (EMbedding L) by ThEME1;

then consider uu being Vector of L such that

A4: (MorphsZQ L) . uu = u by ZMODUL08:22;

(ScProductEM L) . (v,u) = <;vv,uu;> by A1, A2, A3, A4, defScProductEM;

hence (ScProductEM L) . (v,u) is rational ; :: thesis: verum

then consider vv being Vector of L such that

A2: (MorphsZQ L) . vv = v by ZMODUL08:22;

A3: u is Vector of (EMbedding L) by ThEME1;

then consider uu being Vector of L such that

A4: (MorphsZQ L) . uu = u by ZMODUL08:22;

(ScProductEM L) . (v,u) = <;vv,uu;> by A1, A2, A3, A4, defScProductEM;

hence (ScProductEM L) . (v,u) is rational ; :: thesis: verum