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 )

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 )

then ex I being Subset of G st I is base by A3, VECTSP_7:def 3;

then G is free ;

hence ex b_{1} being non trivial Z_Module st b_{1} is free
; :: thesis: verum

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

then
G is Mult-cancelable
;
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;( 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

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

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;
let x be object ; :: thesis: ( x in the carrier of (Lin I) iff x in the carrier of G )

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 H_{1}( Vector of G) -> Element of the carrier of INT.Ring = 0. INT.Ring;

deffunc H_{2}( 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 = H_{1}(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;

Carrier g c= {iv}

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;hereby :: thesis: ( x in the carrier of G implies x in the carrier of (Lin I) )

assume
x in the carrier of G
; :: thesis: 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;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

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 H

deffunc H

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 = H

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

then reconsider g = g as Linear_Combination of G by VECTSP_6:def 1;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;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

Carrier g c= {iv}

proof

then reconsider g = g as Linear_Combination of {iv} by VECTSP_6:def 4;
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;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

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

then ex I being Subset of G st I is base by A3, VECTSP_7:def 3;

then G is free ;

hence ex b