let V be non trivial free Z_Module; :: thesis: for v being non zero Vector of V ex a being Element of INT.Ring ex u being Vector of V st
( a in NAT & a <> 0 & v = a * u & ( for b being Element of INT.Ring
for w being Vector of V st b > a holds
v <> b * w ) )
let v be non zero Vector of V; :: thesis: ex a being Element of INT.Ring ex u being Vector of V st
( a in NAT & a <> 0 & v = a * u & ( for b being Element of INT.Ring
for w being Vector of V st b > a holds
v <> b * w ) )
defpred S₁[ Nat] means ex u being Vector of V ex k being Element of INT.Ring st
( k = $1 & v = k * u );
consider a being Element of INT.Ring such that
A1: ( a in NAT & ( for b being Element of INT.Ring
for u being Vector of V st b > a holds
v <> b * u ) ) by LmND2;
reconsider na = a as Nat by A1;
A2: for k being Nat st S₁[k] holds
k <= na by A1;
A3: ex k being Nat st S₁[k]

proof

take 1 ; :: thesis: S₁[1]
v = (1. INT.Ring) * v by VECTSP_1:def 17;
hence S₁[1] ; :: thesis: verum

end;

consider a0 being Nat such that
A4: ( S₁[a0] & ( for n being Nat st S₁[n] holds
n <= a0 ) ) from NAT_1:sch 6(A2, A3);
reconsider a = a0 as Element of INT.Ring by INT_1:def 2;
consider u being Vector of V such that
A5: v = a * u by A4;
take a ; :: thesis: ex u being Vector of V st
( a in NAT & a <> 0 & v = a * u & ( for b being Element of INT.Ring
for w being Vector of V st b > a holds
v <> b * w ) )
take u ; :: thesis: ( a in NAT & a <> 0 & v = a * u & ( for b being Element of INT.Ring
for w being Vector of V st b > a holds
v <> b * w ) )
thus a in NAT by ORDINAL1:def 12; :: thesis: ( a <> 0 & v = a * u & ( for b being Element of INT.Ring
for w being Vector of V st b > a holds
v <> b * w ) )
thus a <> 0 :: thesis: ( v = a * u & ( for b being Element of INT.Ring
for w being Vector of V st b > a holds
v <> b * w ) )

proof

assume a = 0 ; :: thesis: contradiction
then v = 0. V by A5, ZMODUL01:1;
hence contradiction ; :: thesis: verum

end;

thus v = a * u by A5; :: thesis: for b being Element of INT.Ring
for w being Vector of V st b > a holds
v <> b * w
thus for b being Element of INT.Ring
for w being Vector of V st b > a holds
v <> b * w :: thesis: verum

proof

let b be Element of INT.Ring; :: thesis: for w being Vector of V st b > a holds
v <> b * w
let w be Vector of V; :: thesis: ( b > a implies v <> b * w )
assume B1: b > a ; :: thesis: v <> b * w
b in NAT by B1, INT_1:3;
then reconsider bn = b as Nat ;
not S₁[bn] by A4, B1;
hence v <> b * w ; :: thesis: verum

end;