set AG = INT.Ring ;
set G = ModuleStr(# the carrier of INT.Ring, the addF of INT.Ring, the ZeroF of INT.Ring,(Int-mult-left INT.Ring) #);
reconsider G = ModuleStr(# the carrier of INT.Ring, the addF of INT.Ring, the ZeroF 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 Element of INT.Ring
for v being Vector of G holds
( not a * v = 0. G or a = 0. INT.Ring or v = 0. G )
proof
let a be Element of INT.Ring; :: thesis: for v being Vector of G holds
( not a * v = 0. G or a = 0. INT.Ring or v = 0. G )
let v be Vector of G; :: thesis: ( not a * v = 0. G or a = 0. INT.Ring or v = 0. G )
assume A1: a * v = 0. G ; :: thesis: ( a = 0. INT.Ring or v = 0. G )
reconsider w = v as Element of INT ;
a * w = 0 by A1, Th2;
hence ( a = 0. INT.Ring 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 VECTSP_4:def 2;
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.Ring ;
reconsider a = w as Integer ;
reconsider i0 = 0 as Element of INT.Ring ;
deffunc H1( Vector of G) -> Element of the carrier of INT.Ring = 0. INT.Ring;
deffunc H2( Vector of G) -> Element of INT.Ring = w;
consider g being Function of G,INT.Ring such that
A5: g . iv = w and
A6: for u being Vector of G st u <> iv holds
g . u = H1(u) from FUNCT_2:sch 6();
 reconsider g = g as Element of Funcs ( the carrier of G, the carrier of INT.Ring) by FUNCT_2:8;
now :: thesis: for u being Vector of G st not u in {iv} holds
g . u = 0. INT.Ring
let u be Vector of G; :: thesis: ( not u in {iv} implies g . u = 0. INT.Ring )
assume not u in {iv} ; :: thesis: g . u = 0. INT.Ring
then u <> iv by TARSKI:def 1;
hence g . u = 0. INT.Ring by A6; :: thesis: verum
end;
then reconsider g = g as Linear_Combination of G by VECTSP_6:def 1;
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 Linear_Combination of {iv} by VECTSP_6:def 4;
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 = ModuleStr(# the carrier of G, the addF of G, the ZeroF of G, the lmult of G #) by TARSKI:2, ZMODUL01:47;
then ex I being Subset of G st I is base by A3, VECTSP_7:def 3;
then G is free ;
hence ex b1 being non trivial Z_Module st b1 is free ; :: thesis: verum