let V be RealLinearSpace; :: thesis: for v being VECTOR of V
for L being Linear_Combination of V holds Sum (v + L) = ((sum L) * v) + (Sum L)
let v be VECTOR of V; :: thesis: for L being Linear_Combination of V holds Sum (v + L) = ((sum L) * v) + (Sum L)
let L be Linear_Combination of V; :: thesis: Sum (v + L) = ((sum L) * v) + (Sum L)
defpred S₁[ Nat] means for L being Linear_Combination of V st card (Carrier L) <= $1 holds
Sum (v + L) = ((sum L) * v) + (Sum L);
A1: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A2: S₁[n] ; :: thesis: S₁[n + 1]
let L be Linear_Combination of V; :: thesis: ( card (Carrier L) <= n + 1 implies Sum (v + L) = ((sum L) * v) + (Sum L) )
assume A3: card (Carrier L) <= n + 1 ; :: thesis: Sum (v + L) = ((sum L) * v) + (Sum L)

per cases ( card (Carrier L) <= n or card (Carrier L) = n + 1 ) by A3, NAT_1:8;

suppose card (Carrier L) <= n ; :: thesis: Sum (v + L) = ((sum L) * v) + (Sum L)

hence Sum (v + L) = ((sum L) * v) + (Sum L) by A2; :: thesis: verum

end;

suppose A4: card (Carrier L) = n + 1 ; :: thesis: Sum (v + L) = ((sum L) * v) + (Sum L)

then not Carrier L is empty ;
then consider w being object such that
A5: w in Carrier L ;
reconsider w = w as Element of V by A5;
A6: card ((Carrier L) \ {w}) = n by A4, A5, STIRL2_1:55;
consider Lw being Linear_Combination of {w} such that
A7: Lw . w = L . w by RLVECT_4:37;
set LLw = L - Lw;
(L - Lw) . w = (L . w) - (Lw . w) by RLVECT_2:54
.= 0 by A7 ;
then A8: not w in Carrier (L - Lw) by RLVECT_2:19;
A9: Carrier Lw c= {w} by RLVECT_2:def 6;
then A10: ( Carrier (L - Lw) c= (Carrier L) \/ (Carrier Lw) & (Carrier L) \/ (Carrier Lw) c= (Carrier L) \/ {w} ) by RLVECT_2:55, XBOOLE_1:9;
(Carrier L) \/ {w} = Carrier L by A5, ZFMISC_1:40;
then Carrier (L - Lw) c= Carrier L by A10;
then card (Carrier (L - Lw)) <= n by A8, A6, NAT_1:43, ZFMISC_1:34;
then A11: Sum (v + (L - Lw)) = ((sum (L - Lw)) * v) + (Sum (L - Lw)) by A2;
A12: (L - Lw) + Lw = L + (Lw - Lw) by RLVECT_2:40
.= L + (ZeroLC V) by RLVECT_2:57
.= L by RLVECT_2:41 ;
then A13: Sum L = (Sum (L - Lw)) + (Sum Lw) by RLVECT_3:1
.= (Sum (L - Lw)) + ((Lw . w) * w) by RLVECT_2:32 ;
v + (Carrier Lw) c= v + {w} by A9, RLTOPSP1:8;
then v + (Carrier Lw) c= {(v + w)} by Lm3;
then Carrier (v + Lw) c= {(v + w)} by Th16;
then v + Lw is Linear_Combination of {(v + w)} by RLVECT_2:def 6;
then A14: Sum (v + Lw) = ((v + Lw) . (v + w)) * (v + w) by RLVECT_2:32
.= (Lw . ((v + w) - v)) * (v + w) by Def1
.= (Lw . w) * (v + w) by RLVECT_4:1 ;
A15: sum L = (sum (L - Lw)) + (sum Lw) by A12, Th34
.= (sum (L - Lw)) + (Lw . w) by A9, Th32 ;
v + L = (v + (L - Lw)) + (v + Lw) by A12, Th17;
hence Sum (v + L) = (Sum (v + (L - Lw))) + (Sum (v + Lw)) by RLVECT_3:1
.= (((sum (L - Lw)) * v) + (Sum (L - Lw))) + (((Lw . w) * v) + ((Lw . w) * w)) by A11, A14, RLVECT_1:def 5
.= ((((sum (L - Lw)) * v) + (Sum (L - Lw))) + ((Lw . w) * v)) + ((Lw . w) * w) by RLVECT_1:def 3
.= ((((sum (L - Lw)) * v) + ((Lw . w) * v)) + (Sum (L - Lw))) + ((Lw . w) * w) by RLVECT_1:def 3
.= (((sum L) * v) + (Sum (L - Lw))) + ((Lw . w) * w) by A15, RLVECT_1:def 6
.= ((sum L) * v) + (Sum L) by A13, RLVECT_1:def 3 ;
:: thesis: verum

end;

end;

end;

A16: S₁[ 0 ]

proof

let L be Linear_Combination of V; :: thesis: ( card (Carrier L) <= 0 implies Sum (v + L) = ((sum L) * v) + (Sum L) )
assume card (Carrier L) <= 0 ; :: thesis: Sum (v + L) = ((sum L) * v) + (Sum L)
then A17: Carrier L = {} V ;
then A18: ( L = ZeroLC V & Sum L = 0. V ) by RLVECT_2:34, RLVECT_2:def 5;
v + (Carrier L) = {} by A17, Th8;
then Carrier (v + L) = {} by Th16;
hence Sum (v + L) = 0. V by RLVECT_2:34
.= (0. V) + (0. V)
.= ((sum L) * v) + (Sum L) by A18, Th31, RLVECT_1:10 ;
:: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A16, A1);
then S₁[ card (Carrier L)] ;
hence Sum (v + L) = ((sum L) * v) + (Sum L) ; :: thesis: verum