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 S1[ 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: S1[ 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 ;
then <;u,v;> = 0 by ZMODLAT1:12;
hence <;u,v;> = <;u,w;> by ; :: thesis: verum
end;
A2: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume B1: S1[n] ; :: thesis: S1[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 ;
then B4: card (J \ {s}) = (n + 1) - () by
.= (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 ;
consider l being Linear_Combination of J such that
B7: u = Sum l by ;
reconsider lx = l as Linear_Combination of Js \/ S by ;
consider lx1 being Linear_Combination of Js, lx2 being Linear_Combination of S such that
B8: lx = lx1 + lx2 by ;
B9: u = (Sum lx1) + (Sum lx2) by ;
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
.= (lx2 . s) * <;s,w;> by AS, B2, B3
.= <;(Sum lx2),w;> by ;
thus <;u,v;> = <;(Sum lx1),v;> + <;(Sum lx2),v;> by
.= <;(Sum lx1),w;> + <;(Sum lx2),w;> by B1, B4, B10, B11, B14
.= <;u,w;> by ; :: thesis: verum
end;
A3: for n being Nat holds S1[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 ;
S1[n] by A3;
hence <;u,v;> = <;u,w;> by A4; :: thesis: verum