defpred S₁[ Nat] means for L being Z_Lattice
for l being Linear_Combination of L
for v being Vector of L st card (Carrier l) = $1 holds
<;v,(Sum l);> = SumSc (v,l);
A1: S₁[ 0 ]

proof

let L be Z_Lattice; :: thesis: for l being Linear_Combination of L
for v being Vector of L st card (Carrier l) = 0 holds
<;v,(Sum l);> = SumSc (v,l)
let l be Linear_Combination of L; :: thesis: for v being Vector of L st card (Carrier l) = 0 holds
<;v,(Sum l);> = SumSc (v,l)
let v be Vector of L; :: thesis: ( card (Carrier l) = 0 implies <;v,(Sum l);> = SumSc (v,l) )
assume B1: card (Carrier l) = 0 ; :: thesis: <;v,(Sum l);> = SumSc (v,l)
B2: Carrier l = {} by B1;
then Sum l = 0. L by VECTSP_6:19;
then <;v,(Sum l);> = 0. F_Real by ZMODLAT1:12;
hence <;v,(Sum l);> = SumSc (v,l) by B2, LmSumSc13; :: 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 L be Z_Lattice; :: thesis: for l being Linear_Combination of L
for v being Vector of L st card (Carrier l) = n + 1 holds
<;v,(Sum l);> = SumSc (v,l)
let l be Linear_Combination of L; :: thesis: for v being Vector of L st card (Carrier l) = n + 1 holds
<;v,(Sum l);> = SumSc (v,l)
let v be Vector of L; :: thesis: ( card (Carrier l) = n + 1 implies <;v,(Sum l);> = SumSc (v,l) )
assume B2: card (Carrier l) = 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 L by B3;
B4: card ((Carrier l) \ {u}) = (card (Carrier l)) - (card {u}) by B3, CARD_2:44, ZFMISC_1:31
.= (n + 1) - 1 by B2, CARD_2:42
.= n ;
B5: Carrier l = ((Carrier l) \ {u}) \/ {u} by B3, XBOOLE_1:45, ZFMISC_1:31;
B6: ((Carrier l) \ {u}) /\ {u} = {} by XBOOLE_0:def 7, XBOOLE_1:79;
l is Linear_Combination of Carrier l by VECTSP_6:7;
then consider l1 being Linear_Combination of (Carrier l) \ {u}, l2 being Linear_Combination of {u} such that
B7: l = l1 + l2 by B5, B6, ZMODUL04:26;
Sum l = (Sum l1) + (Sum l2) by B7, ZMODUL02:52;
then B8: <;v,(Sum l);> = <;v,(Sum l1);> + <;v,(Sum l2);> by ZMODLAT1:8;
B9: SumSc (v,l) = (SumSc (v,l1)) + (SumSc (v,l2)) by B7, LmSumSc1X;
for x being Vector of L st x in (Carrier l) \ {u} holds
x in Carrier l1

proof

let x be Vector of L; :: thesis: ( x in (Carrier l) \ {u} implies x in Carrier l1 )
assume C1: x in (Carrier l) \ {u} ; :: thesis: x in Carrier l1
x in Carrier l by C1, XBOOLE_0:def 5;
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 B7, VECTSP_6:22;
not x in Carrier l2 by C1, C3, XBOOLE_0:def 5;
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 B10: Carrier l1 = (Carrier l) \ {u} by VECTSP_6:def 4;
SumSc (v,l2) = <;v,((l2 . u) * u);> by LmSumSc14
.= <;v,(Sum l2);> by VECTSP_6:17 ;
hence <;v,(Sum l);> = SumSc (v,l) by B1, B4, B8, B9, B10; :: thesis: verum

end;

A3: for n being Nat holds S₁[n] from NAT_1:sch 2(A1, A2);
let L be Z_Lattice; :: thesis: for l being Linear_Combination of L
for v being Vector of L holds <;v,(Sum l);> = SumSc (v,l)
let l be Linear_Combination of L; :: thesis: for v being Vector of L holds <;v,(Sum l);> = SumSc (v,l)
let v be Vector of L; :: thesis: <;v,(Sum l);> = SumSc (v,l)
reconsider n = card (Carrier l) as Nat ;
S₁[n] by A3;
hence <;v,(Sum l);> = SumSc (v,l) ; :: thesis: verum