set Z = LatticeStr(# the carrier of (), the addF of (),(0. ()), the lmult of (),() #);
AX: LatticeStr(# the carrier of (), the addF of (),(0. ()), the lmult of (),() #) = GenLat ((),()) ;
then reconsider Z = LatticeStr(# the carrier of (), the addF of (),(0. ()), the lmult of (),() #) 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 b1, b2 being Element of the carrier of Z holds <;b1,b2;> = <;b2,b1;> ) & ( for b1, b2, b3 being Element of the carrier of Z
for b4 being Element of the carrier of INT.Ring holds
( <;(b1 + b2),b3;> = <;b1,b3;> + <;b2,b3;> & <;(b4 * b1),b2;> = b4 * <;b1,b2;> ) ) )
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 () . (x,y) = 0
proof
let y be Vector of Z; :: thesis: () . (x,y) = 0
thus () . (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 b1, b2, b3 being Element of the carrier of Z
for b4 being Element of the carrier of INT.Ring holds
( <;(b1 + b2),b3;> = <;b1,b3;> + <;b2,b3;> & <;(b4 * b1),b2;> = b4 * <;b1,b2;> )
proof
let x, y be Vector of Z; :: thesis: <;x,y;> = <;y,x;>
thus <;x,y;> = () . (x,y)
.= () . (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 () ;
thus <;(x + y),z;> = () . ((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;> = () . ((a * xx),y)
.= a * (() . (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 () & the ZeroF of Z = zeroCoset L & the addF of Z = () || (rng ()) & the lmult of Z = () | [: the carrier of INT.Ring,(rng ()):] & the scalar of Z = ScProductEM L )
thus ( the carrier of Z = rng () & the ZeroF of Z = zeroCoset L & the addF of Z = () || (rng ()) & the lmult of Z = () | [: the carrier of INT.Ring,(rng ()):] & the scalar of Z = ScProductEM L ) by ZMODUL08:def 3; :: thesis: verum