let L be Z_Lattice; :: thesis: ( ( for x being Vector of () st ( for y being Vector of () holds () . (x,y) = 0 ) holds
x = 0. () ) & ( for x, y being Vector of () holds () . (x,y) = () . (y,x) ) & ( for x, y, z being Vector of ()
for a being Element of INT.Ring holds
( () . ((x + y),z) = (() . (x,z)) + (() . (y,z)) & () . ((a * x),y) = a * (() . (x,y)) ) ) )

set Z = EMbedding L;
set f = ScProductEM L;
set T = MorphsZQ L;
thus for x being Vector of () st ( for y being Vector of () holds () . (x,y) = 0 ) holds
x = 0. () :: thesis: ( ( for x, y being Vector of () holds () . (x,y) = () . (y,x) ) & ( for x, y, z being Vector of ()
for a being Element of INT.Ring holds
( () . ((x + y),z) = (() . (x,z)) + (() . (y,z)) & () . ((a * x),y) = a * (() . (x,y)) ) ) )
proof
let x be Vector of (); :: thesis: ( ( for y being Vector of () holds () . (x,y) = 0 ) implies x = 0. () )
assume B1: for y being Vector of () holds () . (x,y) = 0 ; :: thesis: x = 0. ()
consider xx being Vector of L such that
B2: (MorphsZQ L) . xx = x by ZMODUL08:22;
for yy being Vector of L holds <;xx,yy;> = 0
proof
let yy be Vector of L; :: thesis: <;xx,yy;> = 0
(MorphsZQ L) . yy in rng () by FUNCT_2:4;
then reconsider y = () . yy as Vector of () by ZMODUL08:def 3;
(ScProductEM L) . (x,y) = 0 by B1;
hence <;xx,yy;> = 0 by ; :: thesis: verum
end;
hence x = () . (0. L) by
.= Class ((),[(0. L),1]) by ZMODUL04:def 6
.= zeroCoset L by ZMODUL04:def 3
.= 0. () by ZMODUL08:def 3 ;
:: thesis: verum
end;
thus for x, y being Vector of () holds () . (x,y) = () . (y,x) :: thesis: for x, y, z being Vector of ()
for a being Element of INT.Ring holds
( () . ((x + y),z) = (() . (x,z)) + (() . (y,z)) & () . ((a * x),y) = a * (() . (x,y)) )
proof
let x, y be Vector of (); :: thesis: () . (x,y) = () . (y,x)
consider xx being Vector of L such that
B1: (MorphsZQ L) . xx = x by ZMODUL08:22;
consider yy being Vector of L such that
B2: (MorphsZQ L) . yy = y by ZMODUL08:22;
thus () . (x,y) = <;xx,yy;> by
.= <;yy,xx;> by ZMODLAT1:def 3
.= () . (y,x) by ; :: thesis: verum
end;
thus for x, y, z being Vector of ()
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 (); :: 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)) )
consider xx being Vector of L such that
B1: (MorphsZQ L) . xx = x by ZMODUL08:22;
consider yy being Vector of L such that
B2: (MorphsZQ L) . yy = y by ZMODUL08:22;
consider zz being Vector of L such that
B3: (MorphsZQ L) . zz = z by ZMODUL08:22;
B4: () . (xx + yy) = (() . xx) + (() . yy) by ZMODUL04:def 6
.= x + y by ;
reconsider aq = a as Element of F_Rat by NUMBERS:14;
B5: () . (a * xx) = aq * (() . xx) by ZMODUL04:def 6
.= a * x by ;
thus () . ((x + y),z) = <;(xx + yy),zz;> by
.= <;xx,zz;> + <;yy,zz;> by ZMODLAT1:def 3
.= (() . (x,z)) + <;yy,zz;> by
.= (() . (x,z)) + (() . (y,z)) by ; :: thesis: () . ((a * x),y) = a * (() . (x,y))
thus () . ((a * x),y) = <;(a * xx),yy;> by
.= a * <;xx,yy;> by ZMODLAT1:def 3
.= a * (() . (x,y)) by ; :: thesis: verum
end;