let L be positive-definite Z_Lattice; :: thesis: for I being Basis of L
for v, w being Vector of L st ( for u being Vector of L st u in I holds
<;u,v;> = <;u,w;> ) holds
for u being Vector of L holds <;u,v;> = <;u,w;>
let I be Basis of L; :: thesis: for v, w being Vector of L st ( for u being Vector of L st u in I holds
<;u,v;> = <;u,w;> ) holds
for u being Vector of L holds <;u,v;> = <;u,w;>
let v, w be Vector of L; :: thesis: ( ( for u being Vector of L st u in I holds
<;u,v;> = <;u,w;> ) implies for u being Vector of L holds <;u,v;> = <;u,w;> )
assume AS: for u being Vector of L st u in I holds
<;u,v;> = <;u,w;> ; :: thesis: for u being Vector of L holds <;u,v;> = <;u,w;>
defpred S₁[ Nat] means for u being Vector of L
for J being finite Subset of L st J c= I & card J = $1 & u in Lin J holds
<;u,v;> = <;u,w;>;
A1: S₁[ 0 ]

proof

let u be Vector of L; :: thesis: for J being finite Subset of L st J c= I & card J = 0 & u in Lin J holds
<;u,v;> = <;u,w;>
let J be finite Subset of L; :: thesis: ( J c= I & card J = 0 & u in Lin J implies <;u,v;> = <;u,w;> )
assume B1: ( J c= I & card J = 0 & u in Lin J ) ; :: thesis: <;u,v;> = <;u,w;>
J = {} the carrier of L by B1;
then Lin J = (0). L by VECTSP_7:9;
then B2: u = 0. L by B1, VECTSP_4:35;
then <;u,v;> = 0 by ZMODLAT1:12;
hence <;u,v;> = <;u,w;> by B2, ZMODLAT1:12; :: thesis: verum

end;

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

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume B1: S₁[n] ; :: thesis: S₁[n + 1]
let u be Vector of L; :: thesis: for J being finite Subset of L st J c= I & card J = n + 1 & u in Lin J holds
<;u,v;> = <;u,w;>
let J be finite Subset of L; :: thesis: ( J c= I & card J = n + 1 & u in Lin J implies <;u,v;> = <;u,w;> )
assume B2: ( J c= I & card J = n + 1 & u in Lin J ) ; :: thesis: <;u,v;> = <;u,w;>
not J is empty by B2;
then consider s being object such that
B3: s in J ;
reconsider s = s as Vector of L by B3;
set Js = J \ {s};
{s} is Subset of J by B3, SUBSET_1:41;
then B4: card (J \ {s}) = (n + 1) - (card {s}) by B2, CARD_2:44
.= (n + 1) - 1 by CARD_1:30
.= n ;
reconsider Js = J \ {s} as finite Subset of L ;
reconsider S = {s} as finite Subset of L ;
B6: Js /\ S = {} by XBOOLE_0:def 7, XBOOLE_1:79;
consider l being Linear_Combination of J such that
B7: u = Sum l by B2, VECTSP_7:7;
reconsider lx = l as Linear_Combination of Js \/ S by B3, XBOOLE_1:45, ZFMISC_1:31;
consider lx1 being Linear_Combination of Js, lx2 being Linear_Combination of S such that
B8: lx = lx1 + lx2 by B6, ZMODUL04:26;
B9: u = (Sum lx1) + (Sum lx2) by B7, B8, VECTSP_6:44;
B10: Sum lx1 in Lin Js by VECTSP_7:7;
Js c= J by XBOOLE_1:36;
then B11: Js c= I by B2;
B12: Sum lx2 = (lx2 . s) * s by VECTSP_6:17;
B14: <;(Sum lx2),v;> = (lx2 . s) * <;s,v;> by B12, ZMODLAT1:def 3
.= (lx2 . s) * <;s,w;> by AS, B2, B3
.= <;(Sum lx2),w;> by B12, ZMODLAT1:def 3 ;
thus <;u,v;> = <;(Sum lx1),v;> + <;(Sum lx2),v;> by B9, ZMODLAT1:def 3
.= <;(Sum lx1),w;> + <;(Sum lx2),w;> by B1, B4, B10, B11, B14
.= <;u,w;> by B9, ZMODLAT1:def 3 ; :: thesis: verum

end;

A3: for n being Nat holds S₁[n] from NAT_1:sch 2(A1, A2);
let u be Vector of L; :: thesis: <;u,v;> = <;u,w;>
A4: u in Lin I by ZMODUL03:14;
reconsider n = card I as Nat ;
S₁[n] by A3;
hence <;u,v;> = <;u,w;> by A4; :: thesis: verum