set V = the non trivial torsion-free Z_Module;
set v = the non zero Vector of the non trivial torsion-free Z_Module;
set Z = Lin { the non zero Vector of the non trivial torsion-free Z_Module};
defpred S₁[ object , object ] means ex a, b being Element of INT.Ring st
( c₁ = [(a * the non zero Vector of the non trivial torsion-free Z_Module),(b * the non zero Vector of the non trivial torsion-free Z_Module)] & c₂ = a * b );
A1: for x being Element of [: the carrier of (Lin { the non zero Vector of the non trivial torsion-free Z_Module}), the carrier of (Lin { the non zero Vector of the non trivial torsion-free Z_Module}):] ex y being Element of the carrier of F_Real st S₁[x,y]

proof

let x be Element of [: the carrier of (Lin { the non zero Vector of the non trivial torsion-free Z_Module}), the carrier of (Lin { the non zero Vector of the non trivial torsion-free Z_Module}):]; :: thesis: ex y being Element of the carrier of F_Real st S₁[x,y]
consider x1, x2 being object such that
B1: ( x1 in the carrier of (Lin { the non zero Vector of the non trivial torsion-free Z_Module}) & x2 in the carrier of (Lin { the non zero Vector of the non trivial torsion-free Z_Module}) & x = [x1,x2] ) by ZFMISC_1:def 2;
reconsider x1 = x1, x2 = x2 as Vector of (Lin { the non zero Vector of the non trivial torsion-free Z_Module}) by B1;
x1 in Lin { the non zero Vector of the non trivial torsion-free Z_Module} ;
then consider i1 being Element of INT.Ring such that
B2: x1 = i1 * the non zero Vector of the non trivial torsion-free Z_Module by ZMODUL06:19;
x2 in Lin { the non zero Vector of the non trivial torsion-free Z_Module} ;
then consider i2 being Element of INT.Ring such that
B3: x2 = i2 * the non zero Vector of the non trivial torsion-free Z_Module by ZMODUL06:19;
reconsider i12 = i1 * i2 as Element of INT ;
INT c= the carrier of F_Real by NUMBERS:5, XBOOLE_0:def 8;
then reconsider i12 = i12 as Element of the carrier of F_Real ;
take i12 ; :: thesis: S₁[x,i12]
thus S₁[x,i12] by B1, B2, B3; :: thesis: verum

end;

consider f being Function of [: the carrier of (Lin { the non zero Vector of the non trivial torsion-free Z_Module}), the carrier of (Lin { the non zero Vector of the non trivial torsion-free Z_Module}):], the carrier of F_Real such that
A2: for x being Element of [: the carrier of (Lin { the non zero Vector of the non trivial torsion-free Z_Module}), the carrier of (Lin { the non zero Vector of the non trivial torsion-free Z_Module}):] holds S₁[x,f . x] from FUNCT_2:sch 3(A1);
A3: for v1, v2 being Vector of (Lin { the non zero Vector of the non trivial torsion-free Z_Module})
for a, b being Element of INT.Ring st v1 = a * the non zero Vector of the non trivial torsion-free Z_Module & v2 = b * the non zero Vector of the non trivial torsion-free Z_Module holds
f . (v1,v2) = a * b

proof

let v1, v2 be Vector of (Lin { the non zero Vector of the non trivial torsion-free Z_Module}); :: thesis: for a, b being Element of INT.Ring st v1 = a * the non zero Vector of the non trivial torsion-free Z_Module & v2 = b * the non zero Vector of the non trivial torsion-free Z_Module holds
f . (v1,v2) = a * b
let a, b be Element of INT.Ring; :: thesis: ( v1 = a * the non zero Vector of the non trivial torsion-free Z_Module & v2 = b * the non zero Vector of the non trivial torsion-free Z_Module implies f . (v1,v2) = a * b )
assume B0: ( v1 = a * the non zero Vector of the non trivial torsion-free Z_Module & v2 = b * the non zero Vector of the non trivial torsion-free Z_Module ) ; :: thesis: f . (v1,v2) = a * b
consider a0, b0 being Element of INT.Ring such that
B1: ( [v1,v2] = [(a0 * the non zero Vector of the non trivial torsion-free Z_Module),(b0 * the non zero Vector of the non trivial torsion-free Z_Module)] & f . [v1,v2] = a0 * b0 ) by A2;
B2: the non zero Vector of the non trivial torsion-free Z_Module <> 0. the non trivial torsion-free Z_Module ;
v1 = a0 * the non zero Vector of the non trivial torsion-free Z_Module by B1, XTUPLE_0:1;
then B3: a = a0 by B0, B2, ZMODUL01:11;
v2 = b0 * the non zero Vector of the non trivial torsion-free Z_Module by B1, XTUPLE_0:1;
hence f . (v1,v2) = a * b by B0, B1, B2, B3, ZMODUL01:11; :: thesis: verum

end;

set L = GenLat ((Lin { the non zero Vector of the non trivial torsion-free Z_Module}),f);
reconsider L = GenLat ((Lin { the non zero Vector of the non trivial torsion-free Z_Module}),f) as non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed free finite-rank LatticeStr over INT.Ring ;
reconsider L = L as strict Z_Lattice by A3, ThNonTrivialLat1;
take L ; :: thesis: not L is trivial
not L is trivial

proof

assume B1: L is trivial ; :: thesis: contradiction
the non zero Vector of the non trivial torsion-free Z_Module in Lin { the non zero Vector of the non trivial torsion-free Z_Module} by ZMODUL06:20;
then B2: the non zero Vector of the non trivial torsion-free Z_Module = 0. L by B1;
the non zero Vector of the non trivial torsion-free Z_Module <> 0. the non trivial torsion-free Z_Module ;
hence contradiction by B2, ZMODUL01:26; :: thesis: verum

end;

hence not L is trivial ; :: thesis: verum