defpred S1[ Nat] means for L being Z_Lattice
for l being Linear_Combination of DivisibleMod L
for v being Vector of () st card () = \$1 holds
() . (v,(Sum l)) = SumSc (v,l);
A1: S1[ 0 ]
proof
let L be Z_Lattice; :: thesis: for l being Linear_Combination of DivisibleMod L
for v being Vector of () st card () = 0 holds
() . (v,(Sum l)) = SumSc (v,l)

let l be Linear_Combination of DivisibleMod L; :: thesis: for v being Vector of () st card () = 0 holds
() . (v,(Sum l)) = SumSc (v,l)

let v be Vector of (); :: thesis: ( card () = 0 implies () . (v,(Sum l)) = SumSc (v,l) )
assume B1: card () = 0 ; :: thesis: () . (v,(Sum l)) = SumSc (v,l)
B2: Carrier l = {} by B1;
then Sum l = 0. () by VECTSP_6:19;
then (ScProductDM L) . (v,(Sum l)) = 0. F_Real by ZMODLAT2:14;
hence (ScProductDM L) . (v,(Sum l)) = SumSc (v,l) 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 L be Z_Lattice; :: thesis: for l being Linear_Combination of DivisibleMod L
for v being Vector of () st card () = n + 1 holds
() . (v,(Sum l)) = SumSc (v,l)

let l be Linear_Combination of DivisibleMod L; :: thesis: for v being Vector of () st card () = n + 1 holds
() . (v,(Sum l)) = SumSc (v,l)

let v be Vector of (); :: thesis: ( card () = n + 1 implies () . (v,(Sum l)) = SumSc (v,l) )
assume B2: card () = n + 1 ; :: thesis: () . (v,(Sum l)) = SumSc (v,l)
Carrier l <> {} by B2;
then consider u being object such that
B3: u in Carrier l by XBOOLE_0:def 1;
reconsider u = u as Element of () by B3;
B4: card (() \ {u}) = (card ()) - () by
.= (n + 1) - 1 by
.= n ;
B5: Carrier l = (() \ {u}) \/ {u} by ;
B6: ((Carrier l) \ {u}) /\ {u} = {} by ;
l is Linear_Combination of Carrier l by VECTSP_6:7;
then consider l1 being Linear_Combination of () \ {u}, l2 being Linear_Combination of {u} such that
B7: l = l1 + l2 by ;
Sum l = (Sum l1) + (Sum l2) by ;
then B8: (ScProductDM L) . (v,(Sum l)) = (() . (v,(Sum l1))) + (() . (v,(Sum l2))) by ZMODLAT2:12;
for x being Vector of () st x in () \ {u} holds
x in Carrier l1
proof
let x be Vector of (); :: thesis: ( x in () \ {u} implies x in Carrier l1 )
assume C1: x in () \ {u} ; :: thesis: x in Carrier l1
x in Carrier l by ;
then C2: l . x <> 0. INT.Ring by VECTSP_6:2;
C3: Carrier l2 c= {u} by VECTSP_6:def 4;
C4: l . x = (l1 . x) + (l2 . x) by ;
not x in Carrier l2 by ;
then l1 . x <> 0. INT.Ring by C2, C4;
hence x in Carrier l1 ; :: thesis: verum
end;
then (Carrier l) \ {u} c= Carrier l1 ;
then Carrier l1 = () \ {u} by VECTSP_6:def 4;
then B10: (ScProductDM L) . (v,(Sum l1)) = SumSc (v,l1) by B1, B4;
SumSc (v,l2) = () . (v,((l2 . u) * u)) by LmSumScDM14
.= () . (v,(Sum l2)) by VECTSP_6:17 ;
hence (ScProductDM L) . (v,(Sum l)) = SumSc (v,l) by ; :: thesis: verum
end;
A3: for n being Nat holds S1[n] from NAT_1:sch 2(A1, A2);
let L be Z_Lattice; :: thesis: for l being Linear_Combination of DivisibleMod L
for v being Vector of () holds () . (v,(Sum l)) = SumSc (v,l)

let l be Linear_Combination of DivisibleMod L; :: thesis: for v being Vector of () holds () . (v,(Sum l)) = SumSc (v,l)
let v be Vector of (); :: thesis: () . (v,(Sum l)) = SumSc (v,l)
reconsider n = card () as Nat ;
S1[n] by A3;
hence (ScProductDM L) . (v,(Sum l)) = SumSc (v,l) ; :: thesis: verum