let L be Z_Lattice; :: thesis: for I being Subset of L holds
( I is Basis of L iff (MorphsZQ L) .: I is Basis of (EMbedding L) )
let I be Subset of L; :: thesis: ( I is Basis of L iff (MorphsZQ L) .: I is Basis of (EMbedding L) )
consider T being linear-transformation of L,(EMbedding L) such that
A1: T is bijective and
A2: T = MorphsZQ L and
for v being Vector of L holds T . v = Class ((EQRZM L),[v,1]) by ZMODUL08:21;
thus ( I is Basis of L iff (MorphsZQ L) .: I is Basis of (EMbedding L) ) by A1, A2, ZMODUL06:49; :: thesis: verum