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 INT ) holds
for v being Vector of L st v in Lin I holds
<;v,u;> in INT
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 INT ) holds
for v being Vector of L st v in Lin I holds
<;v,u;> in INT
let u be Vector of L; :: thesis: ( ( for v being Vector of L st v in I holds
<;v,u;> in INT ) implies for v being Vector of L st v in Lin I holds
<;v,u;> in INT )
assume AS: for v being Vector of L st v in I holds
<;v,u;> in INT ; :: thesis: for v being Vector of L st v in Lin I holds
<;v,u;> in INT
defpred S₁[ 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 INT ) holds
for v being Vector of L st v in Lin I holds
<;v,u;> in INT ;
P1: S₁[ 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 INT ) implies for v being Vector of L st v in Lin I holds
<;v,u;> in INT )
assume ( card I = 0 & ( for v being Vector of L st v in I holds
<;v,u;> in INT ) ) ; :: thesis: for v being Vector of L st v in Lin I holds
<;v,u;> in INT
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 INT )
assume v in Lin I ; :: thesis: <;v,u;> in INT
then v in {(0. L)} by A2, VECTSP_4:def 3;
then v = 0. L by TARSKI:def 1;
then <;v,u;> = 0 by ThSc6;
hence <;v,u;> in INT ; :: thesis: verum

end;

P2: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A0: S₁[n] ; :: thesis: S₁[n + 1]
thus S₁[n + 1] :: thesis: verum

proof

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 INT ) implies for v being Vector of L st v in Lin I holds
<;v,u;> in INT )
assume A1: ( card I = n + 1 & ( for v being Vector of L st v in I holds
<;v,u;> in INT ) ) ; :: thesis: for v being Vector of L st v in Lin I holds
<;v,u;> in INT
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 A3, ZFMISC_1:40 ;
then A4: Lin I = (Lin (I \ {v})) + (Lin {v}) by ZMODUL02:72;
A5: card (I \ {v}) = (card I) - (card {v}) by A3, CARD_2:44, ZFMISC_1:31
.= (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 INT

proof

let x be Vector of L; :: thesis: ( x in J implies <;x,u;> in INT )
assume x in J ; :: thesis: <;x,u;> in INT
then x in I by XBOOLE_1:36, TARSKI:def 3;
hence <;x,u;> in INT by A1; :: thesis: verum

end;

thus for x being Vector of L st x in Lin I holds
<;x,u;> in INT :: thesis: verum

proof

let x be Vector of L; :: thesis: ( x in Lin I implies <;x,u;> in INT )
assume x in Lin I ; :: thesis: <;x,u;> in INT
then consider xu1, xu2 being Vector of L such that
A10: ( xu1 in Lin (I \ {v}) & xu2 in Lin {v} & x = xu1 + xu2 ) by A4, ZMODUL01:92;
consider ixu2 being Element of INT.Ring such that
A12: xu2 = ixu2 * v by A10, ZMODUL06:19;
B11: x = ((1. INT.Ring) * xu1) + (ixu2 * v) by A10, A12;
set i1 = 1. INT.Ring;
B13: <;x,u;> = ((1. INT.Ring) * <;xu1,u;>) + (ixu2 * <;v,u;>) by B11, ThSc4;
B14: <;xu1,u;> in INT by A0, A5, B8, A10;
<;v,u;> in INT by A1, A3;
hence <;x,u;> in INT by B13, B14, INT_1:def 2; :: thesis: verum

end;

end;

end;

X1: for n being Nat holds S₁[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 INT by X1, AS; :: thesis: verum