set Z = LatticeStr(# the carrier of (EMbedding L), the addF of (EMbedding L),(0. (EMbedding L)), the lmult of (EMbedding L),(ScProductEM L) #);
AX: LatticeStr(# the carrier of (EMbedding L), the addF of (EMbedding L),(0. (EMbedding L)), the lmult of (EMbedding L),(ScProductEM L) #) = GenLat ((EMbedding L),(ScProductEM L)) ;
then reconsider Z = LatticeStr(# the carrier of (EMbedding L), the addF of (EMbedding L),(0. (EMbedding L)), the lmult of (EMbedding L),(ScProductEM L) #) as non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed LatticeStr over INT.Ring ;
reconsider Z = Z as non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed free LatticeStr over INT.Ring by AX;
Z is Z_Lattice-like

proof

thus for x being Vector of Z st ( for y being Vector of Z holds <;x,y;> = 0 ) holds
x = 0. Z :: according to ZMODLAT1:def 3 :: thesis: ( ( for b₁, b₂ being Element of the carrier of Z holds <;b₁,b₂;> = <;b₂,b₁;> ) & ( for b₁, b₂, b₃ being Element of the carrier of Z
for b₄ being Element of the carrier of INT.Ring holds
( <;(b₁ + b₂),b₃;> = <;b₁,b₃;> + <;b₂,b₃;> & <;(b₄ * b₁),b₂;> = b₄ * <;b₁,b₂;> ) ) )

proof

let x be Vector of Z; :: thesis: ( ( for y being Vector of Z holds <;x,y;> = 0 ) implies x = 0. Z )
assume B1: for y being Vector of Z holds <;x,y;> = 0 ; :: thesis: x = 0. Z
for y being Vector of Z holds (ScProductEM L) . (x,y) = 0

proof

let y be Vector of Z; :: thesis: (ScProductEM L) . (x,y) = 0
thus (ScProductEM L) . (x,y) = <;x,y;>
.= 0 by B1 ; :: thesis: verum

end;

hence x = 0. Z by ThSPEM1; :: thesis: verum

end;

thus for x, y being Vector of Z holds <;x,y;> = <;y,x;> :: thesis: for b₁, b₂, b₃ being Element of the carrier of Z
for b₄ being Element of the carrier of INT.Ring holds
( <;(b₁ + b₂),b₃;> = <;b₁,b₃;> + <;b₂,b₃;> & <;(b₄ * b₁),b₂;> = b₄ * <;b₁,b₂;> )

proof

let x, y be Vector of Z; :: thesis: <;x,y;> = <;y,x;>
thus <;x,y;> = (ScProductEM L) . (x,y)
.= (ScProductEM L) . (y,x) by ThSPEM1
.= <;y,x;> ; :: thesis: verum

end;

thus for x, y, z being Vector of Z
for a being Element of INT.Ring holds
( <;(x + y),z;> = <;x,z;> + <;y,z;> & <;(a * x),y;> = a * <;x,y;> ) :: thesis: verum

proof

let x, y, z be Vector of Z; :: thesis: for a being Element of INT.Ring holds
( <;(x + y),z;> = <;x,z;> + <;y,z;> & <;(a * x),y;> = a * <;x,y;> )
let a be Element of INT.Ring; :: thesis: ( <;(x + y),z;> = <;x,z;> + <;y,z;> & <;(a * x),y;> = a * <;x,y;> )
reconsider xx = x, yy = y, zz = z as Vector of (EMbedding L) ;
thus <;(x + y),z;> = (ScProductEM L) . ((xx + yy),zz)
.= ( the scalar of Z . (x,z)) + ( the scalar of Z . (y,z)) by ThSPEM1
.= <;x,z;> + <;y,z;> ; :: thesis: <;(a * x),y;> = a * <;x,y;>
thus <;(a * x),y;> = (ScProductEM L) . ((a * xx),y)
.= a * ((ScProductEM L) . (xx,y)) by ThSPEM1
.= a * <;x,y;> ; :: thesis: verum

end;

end;

then reconsider Z = Z as strict Z_Lattice by AX;
take Z ; :: thesis: ( the carrier of Z = rng (MorphsZQ L) & the ZeroF of Z = zeroCoset L & the addF of Z = (addCoset L) || (rng (MorphsZQ L)) & the lmult of Z = (lmultCoset L) | [: the carrier of INT.Ring,(rng (MorphsZQ L)):] & the scalar of Z = ScProductEM L )
thus ( the carrier of Z = rng (MorphsZQ L) & the ZeroF of Z = zeroCoset L & the addF of Z = (addCoset L) || (rng (MorphsZQ L)) & the lmult of Z = (lmultCoset L) | [: the carrier of INT.Ring,(rng (MorphsZQ L)):] & the scalar of Z = ScProductEM L ) by ZMODUL08:def 3; :: thesis: verum