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

defpred S1[ Nat] means for I being finite Subset of L st card I = \$1 & ( for v, u being Vector of L st v in I & u in I holds
<;v,u;> in RAT ) holds
for v, u being Vector of L st v in Lin I & u 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, u being Vector of L st v in I & u in I holds
<;v,u;> in RAT ) implies for v, u being Vector of L st v in Lin I & u in Lin I holds
<;v,u;> in RAT )

assume ( card I = 0 & ( for v, u being Vector of L st v in I & u in I holds
<;v,u;> in RAT ) ) ; :: thesis: for v, u being Vector of L st v in Lin I & u 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, u be Vector of L; :: thesis: ( v in Lin I & u in Lin I implies <;v,u;> in RAT )
assume ( v in Lin I & u in Lin I ) ; :: thesis: <;v,u;> in RAT
then ( v in {(0. L)} & u in {(0. L)} ) by ;
then ( v = 0. L & u = 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, u being Vector of L st v in I & u in I holds
<;v,u;> in RAT ) implies for v, u being Vector of L st v in Lin I & u in Lin I holds
<;v,u;> in RAT )

assume A1: ( card I = n + 1 & ( for v, u being Vector of L st v in I & u in I holds
<;v,u;> in RAT ) ) ; :: thesis: for v, u being Vector of L st v in Lin I & u 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, y being Vector of L st x in J & y in J holds
<;x,y;> in RAT
proof
let x, y be Vector of L; :: thesis: ( x in J & y in J implies <;x,y;> in RAT )
assume ( x in J & y in J ) ; :: thesis: <;x,y;> in RAT
then ( x in I & y in I ) by ;
hence <;x,y;> in RAT by A1; :: thesis: verum
end;
A6X: for x being Vector of L st x in J holds
<;x,v;> in RAT
proof
let x be Vector of L; :: thesis: ( x in J implies <;x,v;> in RAT )
assume x in J ; :: thesis: <;x,v;> in RAT
then ( x in I & v in I ) by ;
hence <;x,v;> in RAT by A1; :: thesis: verum
end;
thus for x, y being Vector of L st x in Lin I & y in Lin I holds
<;x,y;> in RAT :: thesis: verum
proof
let x, y be Vector of L; :: thesis: ( x in Lin I & y in Lin I implies <;x,y;> in RAT )
assume A9: ( x in Lin I & y in Lin I ) ; :: thesis: <;x,y;> 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 yu1, yu2 being Vector of L such that
A11: ( yu1 in Lin (I \ {v}) & yu2 in Lin {v} & y = yu1 + yu2 ) by ;
consider ixu2 being Element of INT.Ring such that
A12: xu2 = ixu2 * v by ;
consider iyu2 being Element of INT.Ring such that
A13: yu2 = iyu2 * v by ;
B11: x = (() * xu1) + (ixu2 * v) by ;
set i1 = 1. INT.Ring;
B13: <;x,y;> = <;((() * xu1) + (ixu2 * v)),yu1;> + <;((() * xu1) + (ixu2 * v)),(iyu2 * v);> by
.= ((() * <;xu1,yu1;>) + (ixu2 * <;v,yu1;>)) + <;((() * xu1) + (ixu2 * v)),(iyu2 * v);> by ZMODLAT1:10
.= ((() * <;xu1,yu1;>) + (ixu2 * <;v,yu1;>)) + ((() * <;xu1,(iyu2 * v);>) + (ixu2 * <;v,(iyu2 * v);>)) by ZMODLAT1:10
.= ((<;xu1,yu1;> + (ixu2 * <;v,yu1;>)) + <;xu1,(iyu2 * v);>) + (ixu2 * <;v,(iyu2 * v);>)
.= ((<;xu1,yu1;> + (ixu2 * <;v,yu1;>)) + <;xu1,(iyu2 * v);>) + (ixu2 * (iyu2 * <;v,v;>)) by ZMODLAT1:9
.= ((<;xu1,yu1;> + (ixu2 * <;v,yu1;>)) + (iyu2 * <;xu1,v;>)) + ((ixu2 * iyu2) * <;v,v;>) by ZMODLAT1:9 ;
B14: <;xu1,yu1;> in RAT by A0, A5, B8, A10, A11;
<;yu1,v;> in RAT by ;
then B15: <;v,yu1;> in RAT by ZMODLAT1:def 3;
B16: <;xu1,v;> in RAT by ;
<;v,v;> in RAT by A3, A1;
hence <;x,y;> in RAT by ; :: thesis: verum
end;
end;
X1: for n being Nat holds S1[n] from NAT_1:sch 2(P1, P2);
let I be Basis of L; :: thesis: ( ( for v, u being Vector of L st v in I & u in I holds
<;v,u;> in RAT ) implies for v, u being Vector of L holds <;v,u;> in RAT )

assume X2: for v, u being Vector of L st v in I & u in I holds
<;v,u;> in RAT ; :: thesis: for v, u being Vector of L holds <;v,u;> in RAT
X3: ( I is linearly-independent & Lin I = ModuleStr(# the carrier of L, the addF of L, the ZeroF of L, the lmult of L #) ) by VECTSP_7:def 3;
X4: card I is Nat ;
let v, u be Vector of L; :: thesis: <;v,u;> in RAT
( v in Lin I & u in Lin I ) by X3;
hence <;v,u;> in RAT by X1, X2, X4; :: thesis: verum