set Z = EMLat L;

for v, u being Vector of (EMLat L) holds <;v,u;> in INT

for v, u being Vector of (EMLat L) holds <;v,u;> in INT

proof

hence
EMLat L is INTegral
; :: thesis: verum
let v, u be Vector of (EMLat L); :: thesis: <;v,u;> in INT

v in the carrier of (EMLat L) ;

then v in rng (MorphsZQ L) by defEMLat;

then B3: v is Vector of (EMbedding L) by ZMODUL08:def 3;

then consider vv being Vector of L such that

B1: (MorphsZQ L) . vv = v by ZMODUL08:22;

u in the carrier of (EMLat L) ;

then u in rng (MorphsZQ L) by defEMLat;

then B4: u is Vector of (EMbedding L) by ZMODUL08:def 3;

then consider uu being Vector of L such that

B2: (MorphsZQ L) . uu = u by ZMODUL08:22;

<;v,u;> = (ScProductEM L) . (v,u) by defEMLat

.= <;vv,uu;> by B1, B2, B3, B4, defScProductEM ;

hence <;v,u;> in INT by ZMODLAT1:def 5; :: thesis: verum

end;v in the carrier of (EMLat L) ;

then v in rng (MorphsZQ L) by defEMLat;

then B3: v is Vector of (EMbedding L) by ZMODUL08:def 3;

then consider vv being Vector of L such that

B1: (MorphsZQ L) . vv = v by ZMODUL08:22;

u in the carrier of (EMLat L) ;

then u in rng (MorphsZQ L) by defEMLat;

then B4: u is Vector of (EMbedding L) by ZMODUL08:def 3;

then consider uu being Vector of L such that

B2: (MorphsZQ L) . uu = u by ZMODUL08:22;

<;v,u;> = (ScProductEM L) . (v,u) by defEMLat

.= <;vv,uu;> by B1, B2, B3, B4, defScProductEM ;

hence <;v,u;> in INT by ZMODLAT1:def 5; :: thesis: verum