set AG = INT.Ring ;
set G = Z_ModuleStruct(# the carrier of INT.Ring, the ZeroF of INT.Ring, the addF of INT.Ring,(Int-mult-left INT.Ring) #);
reconsider G = Z_ModuleStruct(# the carrier of INT.Ring, the ZeroF of INT.Ring, the addF of INT.Ring,(Int-mult-left INT.Ring) #) as non trivial Z_Module by ZMODUL01:164;
reconsider iv = 1 as VECTOR of G ;
reconsider i1 = 1 as Element of INT by INT_1:def 2;
set I = {iv};
reconsider I = {iv} as Subset of G ;
for a being Integer
for v being VECTOR of G holds
( not a * v = 0. G or a = 0 or v = 0. G )

proof

let a be Integer; :: thesis: for v being VECTOR of G holds
( not a * v = 0. G or a = 0 or v = 0. G )
let v be VECTOR of G; :: thesis: ( not a * v = 0. G or a = 0 or v = 0. G )
assume A1: a * v = 0. G ; :: thesis: ( a = 0 or v = 0. G )
reconsider w = v as Element of INT ;
A2: a is Element of INT by INT_1:def 2;
a * w = 0 by A1, A2, Th2;
hence ( a = 0 or v = 0. G ) by XCMPLX_1:6; :: thesis: verum

end;

then G is Mult-cancelable ;
then A3: I is linearly-independent by ZMODUL02:59;
for x being object holds
( x in the carrier of (Lin I) iff x in the carrier of G )

proof

let x be object ; :: thesis: ( x in the carrier of (Lin I) iff x in the carrier of G )

hereby :: thesis: ( x in the carrier of G implies x in the carrier of (Lin I) )

assume A4: x in the carrier of (Lin I) ; :: thesis: x in the carrier of G
the carrier of (Lin I) c= the carrier of G by ZMODUL01:def 9;
hence x in the carrier of G by A4; :: thesis: verum

end;

assume x in the carrier of G ; :: thesis: x in the carrier of (Lin I)
then reconsider v0 = x as VECTOR of G ;
reconsider w = v0 as Element of INT ;
reconsider a = w as Integer ;
reconsider i0 = 0 as Element of INT by INT_1:def 2;
deffunc H₁( VECTOR of G) -> Element of INT = i0;
deffunc H₂( VECTOR of G) -> Element of INT = w;
consider g being Function of the carrier of G,INT such that
A5: g . iv = w and
A6: for u being VECTOR of G st u <> iv holds
g . u = H₁(u) from FUNCT_2:sch 6();
reconsider g = g as Element of Funcs ( the carrier of G,INT) by FUNCT_2:8;

now :: thesis: for u being VECTOR of G st not u in {iv} holds
g . u = 0

let u be VECTOR of G; :: thesis: ( not u in {iv} implies g . u = 0 )
assume not u in {iv} ; :: thesis: g . u = 0
then u <> iv by TARSKI:def 1;
hence g . u = 0 by A6; :: thesis: verum

end;

then reconsider g = g as Z_Linear_Combination of G by ZMODUL02:def 18;
Carrier g c= {iv}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Carrier g or x in {iv} )
assume x in Carrier g ; :: thesis: x in {iv}
then ex u being VECTOR of G st
( x = u & g . u <> 0 ) ;
then x = iv by A6;
hence x in {iv} by TARSKI:def 1; :: thesis: verum

end;

then reconsider g = g as Z_Linear_Combination of {iv} by ZMODUL02:def 21;
Sum g = w * iv by A5, ZMODUL02:21
.= w * i1 by Th2
.= v0 ;
hence x in the carrier of (Lin I) by STRUCT_0:def 5, ZMODUL02:64; :: thesis: verum

end;

then Lin I = Z_ModuleStruct(# the carrier of G, the ZeroF of G, the addF of G, the Mult of G #) by TARSKI:2, ZMODUL01:47;
then G is free by A3;
hence ex b₁ being non trivial Z_Module st b₁ is free ; :: thesis: verum