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 D = DivisibleMod L;
set Z = EMbedding L;
set f = ScProductDM L;
A1: EMbedding L is Submodule of DivisibleMod L by ZMODUL08:24;
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 a being Element of INT.Ring such that
B2: ( a <> 0. INT.Ring & a * x in EMbedding L ) by ZMODUL08:29;
reconsider xx = a * x as Vector of () by B2;
for yy being Vector of () holds () . (xx,yy) = 0
proof
let yy be Vector of (); :: thesis: () . (xx,yy) = 0
set b = 1. INT.Ring;
yy in EMbedding L ;
then yy in DivisibleMod L by ;
then reconsider y = () * yy as Vector of () by VECTSP_1:def 17;
y = yy by VECTSP_1:def 17;
then C1: ( 1. INT.Ring <> 0 & yy = () * y ) by VECTSP_1:def 17;
INT c= the carrier of F_Real by NUMBERS:5;
then reconsider af = a, bf = 1. INT.Ring as Element of F_Real ;
C2: (ScProductDM L) . (x,y) = ((af ") * (bf ")) * (() . (xx,yy)) by ;
thus (ScProductEM L) . (xx,yy) = 0 :: thesis: verum
proof
assume (ScProductEM L) . (xx,yy) <> 0 ; :: thesis: contradiction
then XX1: ( af " = 0 or bf " = 0 ) by B1, C2;
( af <> 0. F_Real & bf <> 0. F_Real ) by B2;
hence contradiction by XX1, VECTSP_1:25; :: thesis: verum
end;
end;
then xx = 0. () by ThSPEM1
.= 0. () by ;
hence x = 0. () by ; :: 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 a being Element of INT.Ring such that
B1: ( a <> 0 & a * x in EMbedding L ) by ZMODUL08:29;
reconsider xx = a * x as Vector of () by B1;
consider b being Element of INT.Ring such that
B2: ( b <> 0 & b * y in EMbedding L ) by ZMODUL08:29;
reconsider yy = b * y as Vector of () by B2;
INT c= the carrier of F_Real by NUMBERS:5;
then reconsider af = a, bf = b as Element of F_Real ;
thus () . (x,y) = ((af ") * (bf ")) * (() . (xx,yy)) by
.= ((bf ") * (af ")) * (() . (yy,xx)) by ThSPEM1
.= () . (y,x) by ; :: thesis: verum
end;
thus for x, y, z being Vector of ()
for i being Element of INT.Ring holds
( () . ((x + y),z) = (() . (x,z)) + (() . (y,z)) & () . ((i * x),y) = i * (() . (x,y)) ) :: thesis: verum
proof
let x, y, z be Vector of (); :: thesis: for i being Element of INT.Ring holds
( () . ((x + y),z) = (() . (x,z)) + (() . (y,z)) & () . ((i * x),y) = i * (() . (x,y)) )

let i be Element of INT.Ring; :: thesis: ( () . ((x + y),z) = (() . (x,z)) + (() . (y,z)) & () . ((i * x),y) = i * (() . (x,y)) )
consider a being Element of INT.Ring such that
B1: ( a <> 0 & a * x in EMbedding L ) by ZMODUL08:29;
reconsider xx = a * x as Vector of () by B1;
consider b being Element of INT.Ring such that
B2: ( b <> 0 & b * y in EMbedding L ) by ZMODUL08:29;
reconsider yy = b * y as Vector of () by B2;
consider c being Element of INT.Ring such that
B3: ( c <> 0 & c * z in EMbedding L ) by ZMODUL08:29;
reconsider zz = c * z as Vector of () by B3;
B41: b * (a * x) = b * xx by ;
B42: a * (b * y) = a * yy by ;
B4: (a * b) * (x + y) = ((a * b) * x) + ((a * b) * y) by VECTSP_1:def 14
.= ((b * a) * x) + (a * (b * y)) by VECTSP_1:def 16
.= (b * (a * x)) + (a * (b * y)) by VECTSP_1:def 16
.= (b * xx) + (a * yy) by ;
then reconsider xy = (a * b) * (x + y) as Vector of () ;
INT c= the carrier of F_Real by NUMBERS:5;
then reconsider af = a, bf = b, cf = c as Element of F_Real ;
X2: ( af <> 0. F_Real & bf <> 0. F_Real ) by B1, B2;
then X1: ((af * bf) ") * (cf ") = ((af ") * (bf ")) * (cf ") by VECTSP_2:11;
thus () . ((x + y),z) = (((af ") * (bf ")) * (cf ")) * (() . (xy,zz)) by
.= (((af ") * (bf ")) * (cf ")) * ((() . ((b * xx),zz)) + (() . ((a * yy),zz))) by
.= ((((af ") * (bf ")) * (cf ")) * (() . ((b * xx),zz))) + ((((af ") * (bf ")) * (cf ")) * (() . ((a * yy),zz)))
.= ((((af ") * (bf ")) * (cf ")) * (b * (() . (xx,zz)))) + ((((af ") * (bf ")) * (cf ")) * (() . ((a * yy),zz))) by ThSPEM1
.= ((((af ") * ((bf ") * bf)) * (cf ")) * (() . (xx,zz))) + ((((af ") * (bf ")) * (cf ")) * (() . ((a * yy),zz)))
.= ((((af ") * ()) * (cf ")) * (() . (xx,zz))) + ((((af ") * (bf ")) * (cf ")) * (() . ((a * yy),zz))) by
.= (((af ") * (cf ")) * (() . (xx,zz))) + ((((af ") * (bf ")) * (cf ")) * (a * (() . (yy,zz)))) by ThSPEM1
.= (((af ") * (cf ")) * (() . (xx,zz))) + ((((bf ") * (af * (af "))) * (cf ")) * (() . (yy,zz)))
.= (((af ") * (cf ")) * (() . (xx,zz))) + ((((bf ") * ()) * (cf ")) * (() . (yy,zz))) by
.= (() . (x,z)) + (((bf ") * (cf ")) * (() . (yy,zz))) by
.= (() . (x,z)) + (() . (y,z)) by ; :: thesis: () . ((i * x),y) = i * (() . (x,y))
a * (i * x) = (a * i) * x by VECTSP_1:def 16
.= i * (a * x) by VECTSP_1:def 16
.= i * xx by ;
hence () . ((i * x),y) = ((af ") * (bf ")) * (() . ((i * xx),yy)) by
.= ((af ") * (bf ")) * (i * (() . (xx,yy))) by ThSPEM1
.= i * (((af ") * (bf ")) * (() . (xx,yy)))
.= i * (() . (x,y)) by ;
:: thesis: verum
end;