let L be Z_Lattice; :: thesis: for I being finite Subset of L
for u being Vector of L st ( for v being Vector of L st v in I holds
<;v,u;> in RAT ) holds
for v being Vector of L st v in Lin I holds
<;v,u;> in RAT

let I be finite Subset of L; :: thesis: for u being Vector of L st ( for v being Vector of L st v in I holds
<;v,u;> in RAT ) holds
for v being Vector of L st v in Lin I holds
<;v,u;> in RAT

let u be Vector of L; :: thesis: ( ( for v being Vector of L st v in I holds
<;v,u;> in RAT ) implies for v being Vector of L st v in Lin I holds
<;v,u;> in RAT )

assume AS: for v being Vector of L st v in I holds
<;v,u;> in RAT ; :: thesis: for v being Vector of L st v in Lin I holds
<;v,u;> in RAT

defpred S1[ Nat] means for I being finite Subset of L st card I = \$1 & ( for v being Vector of L st v in I holds
<;v,u;> in RAT ) holds
for v being Vector of L st v in Lin I holds
<;v,u;> in RAT ;
P1: S1[ 0 ]
proof
let I be finite Subset of L; :: thesis: ( card I = 0 & ( for v being Vector of L st v in I holds
<;v,u;> in RAT ) implies for v being Vector of L st v in Lin I holds
<;v,u;> in RAT )

assume ( card I = 0 & ( for v being Vector of L st v in I holds
<;v,u;> in RAT ) ) ; :: thesis: for v being Vector of L st v in Lin I holds
<;v,u;> in RAT

then I = {} the carrier of L ;
then A2: Lin I = (0). L by ZMODUL02:67;
let v be Vector of L; :: thesis: ( v in Lin I implies <;v,u;> in RAT )
assume v in Lin I ; :: thesis: <;v,u;> in RAT
then v in {(0. L)} by ;
then v = 0. L by TARSKI:def 1;
then <;v,u;> = 0 by ZMODLAT1:12;
hence <;v,u;> in RAT by RAT_1:def 2; :: thesis: verum
end;
P2: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume A0: S1[n] ; :: thesis: S1[n + 1]
let I be finite Subset of L; :: thesis: ( card I = n + 1 & ( for v being Vector of L st v in I holds
<;v,u;> in RAT ) implies for v being Vector of L st v in Lin I holds
<;v,u;> in RAT )

assume A1: ( card I = n + 1 & ( for v being Vector of L st v in I holds
<;v,u;> in RAT ) ) ; :: thesis: for v being Vector of L st v in Lin I holds
<;v,u;> in RAT

then I <> {} ;
then consider v being object such that
A3: v in I by XBOOLE_0:def 1;
reconsider v = v as Vector of L by A3;
(I \ {v}) \/ {v} = I \/ {v} by XBOOLE_1:39
.= I by ;
then A4: Lin I = (Lin (I \ {v})) + () by ZMODUL02:72;
A5: card (I \ {v}) = (card I) - () by
.= (card I) - 1 by CARD_1:30
.= n by A1 ;
reconsider J = I \ {v} as finite Subset of L ;
B8: for x being Vector of L st x in J holds
<;x,u;> in RAT
proof
let x be Vector of L; :: thesis: ( x in J implies <;x,u;> in RAT )
assume x in J ; :: thesis: <;x,u;> in RAT
then x in I by ;
hence <;x,u;> in RAT by A1; :: thesis: verum
end;
thus for x being Vector of L st x in Lin I holds
<;x,u;> in RAT :: thesis: verum
proof
let x be Vector of L; :: thesis: ( x in Lin I implies <;x,u;> in RAT )
assume x in Lin I ; :: thesis: <;x,u;> in RAT
then consider xu1, xu2 being Vector of L such that
A10: ( xu1 in Lin (I \ {v}) & xu2 in Lin {v} & x = xu1 + xu2 ) by ;
consider ixu2 being Element of INT.Ring such that
A12: xu2 = ixu2 * v by ;
B11: x = (() * xu1) + (ixu2 * v) by ;
set i1 = 1. INT.Ring;
B13: <;x,u;> = (() * <;xu1,u;>) + (ixu2 * <;v,u;>) by ;
B14: <;xu1,u;> in RAT by A0, A5, B8, A10;
<;v,u;> in RAT by A1, A3;
hence <;x,u;> in RAT by ; :: thesis: verum
end;
end;
X1: for n being Nat holds S1[n] from NAT_1:sch 2(P1, P2);
card I is Nat ;
hence for v being Vector of L st v in Lin I holds
<;v,u;> in RAT by X1, AS; :: thesis: verum