let L be Z_Lattice; :: thesis: ScProductEM L = (ScProductDM L) || (rng (MorphsZQ L))
P1: [: the carrier of (EMbedding L), the carrier of (EMbedding L):] = [: the carrier of (EMbedding L),(rng (MorphsZQ L)):] by ZMODUL08:def 3
.= [:(rng (MorphsZQ L)),(rng (MorphsZQ L)):] by ZMODUL08:def 3 ;
P2: [: the carrier of (DivisibleMod L), the carrier of (DivisibleMod L):] = [: the carrier of (DivisibleMod L),(Class (EQRZM L)):] by ZMODUL08:def 4
.= [:(Class (EQRZM L)),(Class (EQRZM L)):] by ZMODUL08:def 4 ;
A0: EMbedding L is Submodule of DivisibleMod L by ZMODUL08:24;
then the carrier of (EMbedding L) c= the carrier of (DivisibleMod L) by VECTSP_4:def 2;
then rng (MorphsZQ L) c= the carrier of (DivisibleMod L) by ZMODUL08:def 3;
then rng (MorphsZQ L) c= Class (EQRZM L) by ZMODUL08:def 4;
then [:(rng (MorphsZQ L)),(rng (MorphsZQ L)):] c= [:(Class (EQRZM L)),(Class (EQRZM L)):] by ZFMISC_1:96;
then reconsider scd = (ScProductDM L) || (rng (MorphsZQ L)) as Function of [:(rng (MorphsZQ L)),(rng (MorphsZQ L)):], the carrier of F_Real by P2, FUNCT_2:32;
for x being object st x in [:(rng (MorphsZQ L)),(rng (MorphsZQ L)):] holds
(ScProductEM L) . x = scd . x

proof

let x be object ; :: thesis: ( x in [:(rng (MorphsZQ L)),(rng (MorphsZQ L)):] implies (ScProductEM L) . x = scd . x )
assume B1: x in [:(rng (MorphsZQ L)),(rng (MorphsZQ L)):] ; :: thesis: (ScProductEM L) . x = scd . x
consider x1, x2 being object such that
B2: ( x1 in rng (MorphsZQ L) & x2 in rng (MorphsZQ L) & x = [x1,x2] ) by B1, ZFMISC_1:def 2;
reconsider x1 = x1, x2 = x2 as Vector of (EMbedding L) by B2, ZMODUL08:def 3;
set a = 1. INT.Ring;
x1 in EMbedding L ;
then x1 in DivisibleMod L by A0, ZMODUL01:24;
then reconsider xx1 = x1 as Vector of (DivisibleMod L) ;
x2 in EMbedding L ;
then x2 in DivisibleMod L by A0, ZMODUL01:24;
then reconsider xx2 = x2 as Vector of (DivisibleMod L) ;
B3: x1 = (1. INT.Ring) * xx1 ;
B4: x2 = (1. INT.Ring) * xx2 ;
thus (ScProductEM L) . x = ((1. F_Real) * ((1. F_Real) ")) * ((ScProductEM L) . (x1,x2)) by B2
.= (ScProductDM L) . (xx1,xx2) by B3, B4, defScProductDM
.= scd . x by B2, FUNCT_1:49, ZFMISC_1:87 ; :: thesis: verum

end;

hence ScProductEM L = (ScProductDM L) || (rng (MorphsZQ L)) by P1, FUNCT_2:12; :: thesis: verum