let L be Z_Lattice; :: thesis: for v being Vector of ()
for I being Basis of () st ( for u being Vector of () st u in I holds
() . (v,u) = 0 ) holds
for u being Vector of () holds () . (v,u) = 0

let v be Vector of (); :: thesis: for I being Basis of () st ( for u being Vector of () st u in I holds
() . (v,u) = 0 ) holds
for u being Vector of () holds () . (v,u) = 0

let I be Basis of (); :: thesis: ( ( for u being Vector of () st u in I holds
() . (v,u) = 0 ) implies for u being Vector of () holds () . (v,u) = 0 )

assume A1: for u being Vector of () st u in I holds
() . (v,u) = 0 ; :: thesis: for u being Vector of () holds () . (v,u) = 0
defpred S1[ Nat] means for I being finite Subset of () st card I = \$1 & I is linearly-independent & ( for u being Vector of () st u in I holds
() . (v,u) = 0 ) holds
for w being Vector of () st w in Lin I holds
() . (v,w) = 0 ;
P1: S1[ 0 ]
proof
let I be finite Subset of (); :: thesis: ( card I = 0 & I is linearly-independent & ( for u being Vector of () st u in I holds
() . (v,u) = 0 ) implies for w being Vector of () st w in Lin I holds
() . (v,w) = 0 )

assume B1: ( card I = 0 & I is linearly-independent & ( for u being Vector of () st u in I holds
() . (v,u) = 0 ) ) ; :: thesis: for w being Vector of () st w in Lin I holds
() . (v,w) = 0

I = {} the carrier of () by B1;
then B2: Lin I = (0). () by ZMODUL02:67;
thus for w being Vector of () st w in Lin I holds
() . (v,w) = 0 :: thesis: verum
proof
let w be Vector of (); :: thesis: ( w in Lin I implies () . (v,w) = 0 )
assume C1: w in Lin I ; :: thesis: () . (v,w) = 0
w = 0. () by
.= zeroCoset L by ZMODUL08:def 3
.= 0. () by ZMODUL08:def 4 ;
hence (ScProductDM L) . (v,w) = 0 by ThScDM6; :: thesis: verum
end;
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 B1: S1[n] ; :: thesis: S1[n + 1]
let I be finite Subset of (); :: thesis: ( card I = n + 1 & I is linearly-independent & ( for u being Vector of () st u in I holds
() . (v,u) = 0 ) implies for w being Vector of () st w in Lin I holds
() . (v,w) = 0 )

assume B2: ( card I = n + 1 & I is linearly-independent & ( for u being Vector of () st u in I holds
() . (v,u) = 0 ) ) ; :: thesis: for w being Vector of () st w in Lin I holds
() . (v,w) = 0

not I is empty by B2;
then consider u being object such that
B3: u in I ;
reconsider u = u as Vector of () by B3;
set Iu = I \ {u};
{u} is Subset of I by ;
then B4: card (I \ {u}) = (n + 1) - () by
.= (n + 1) - 1 by CARD_1:30
.= n ;
reconsider Iu = I \ {u} as finite Subset of () ;
I = Iu \/ {u} by ;
then B5: Lin I = (Lin Iu) + () by ZMODUL02:72;
B7: Iu c= I by XBOOLE_1:36;
B6: Iu is linearly-independent by ;
B8: for w being Vector of () st w in Iu holds
() . (v,w) = 0 by B2, B7;
thus for w being Vector of () st w in Lin I holds
() . (v,w) = 0 :: thesis: verum
proof
let w be Vector of (); :: thesis: ( w in Lin I implies () . (v,w) = 0 )
assume C1: w in Lin I ; :: thesis: () . (v,w) = 0
consider w1, w2 being Vector of () such that
C2: ( w1 in Lin Iu & w2 in Lin {u} & w = w1 + w2 ) by ;
CX: EMbedding L is Submodule of DivisibleMod L by ZMODUL08:24;
then C9: w1 is Vector of () by ZMODUL01:25;
reconsider ww1 = w1 as Vector of () by ;
consider i being Element of INT.Ring such that
C4: w2 = i * u by ;
u is Element of () by ;
then C6: (ScProductDM L) . (v,u) = 0 by B2, B3;
reconsider uu = u as Element of () by ;
i * uu in DivisibleMod L ;
then reconsider ww2 = w2 as Vector of () by ;
C8: () . (v,(i * u)) = () . (v,(i * uu)) by
.= () . ((i * uu),v) by ThSPDM1
.= i * (() . (uu,v)) by ThSPDM1
.= i * (() . (v,u)) by ThSPDM1 ;
C10: w = ww1 + ww2 by ;
() . (v,w) = () . (w,v) by ThSPDM1
.= (() . (ww1,v)) + (() . (ww2,v)) by
.= (() . (v,w1)) + (() . (ww2,v)) by ThSPDM1
.= (() . (v,w1)) + (() . (v,w2)) by ThSPDM1 ;
hence (ScProductDM L) . (v,w) = 0 by B1, B4, B6, B8, C2, C4, C6, C8, C9; :: thesis: verum
end;
end;
P3: for n being Nat holds S1[n] from NAT_1:sch 2(P1, P2);
P4: card I is Nat ;
P5: ( I is linearly-independent & EMbedding L = Lin I ) by VECTSP_7:def 3;
thus for w being Vector of () holds () . (v,w) = 0 :: thesis: verum
proof
let w be Vector of (); :: thesis: () . (v,w) = 0
consider a being Element of INT.Ring such that
B1: ( a <> 0. INT.Ring & a * w in EMbedding L ) by ZMODUL08:29;
() . (v,(a * w)) = () . ((a * w),v) by ThSPDM1
.= a * (() . (w,v)) by ThSPDM1
.= a * (() . (v,w)) by ThSPDM1 ;
hence (ScProductDM L) . (v,w) = 0 by A1, B1, P3, P4, P5; :: thesis: verum
end;