let V be free Z_Module; :: thesis: for sc being Function of [: the carrier of V, the carrier of V:], the carrier of F_Real holds GenLat (V,sc) is free
let sc be Function of [: the carrier of V, the carrier of V:], the carrier of F_Real; :: thesis: GenLat (V,sc) is free
set L = GenLat (V,sc);
consider A being Subset of V such that
AX2: A is base by VECTSP_7:def 4;
reconsider AA = A as Subset of (GenLat (V,sc)) ;
A4: GenLat (V,sc) is Submodule of V by LmZMtoZL1;
A5: AA is linearly-independent by AX2, A4, VECTSP_7:def 3, ZMODUL03:16;
Lin AA = Lin A by A4, ZMODUL03:20
.= (Omega). (GenLat (V,sc)) by AX2, VECTSP_7:def 3 ;
hence GenLat (V,sc) is free by A5, VECTSP_7:def 3, VECTSP_7:def 4; :: thesis: verum