let r be Real; :: thesis: for V being RealLinearSpace
for L being Linear_Combination of V holds Sum (r (*) L) = r * (Sum L)
let V be RealLinearSpace; :: thesis: for L being Linear_Combination of V holds Sum (r (*) L) = r * (Sum L)
let L be Linear_Combination of V; :: thesis: Sum (r (*) L) = r * (Sum L)
defpred S₁[ Nat] means for L being Linear_Combination of V st card (Carrier L) <= $1 holds
Sum (r (*) L) = r * (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 (r (*) L) = r * (Sum L) )
assume A3: card (Carrier L) <= n + 1 ; :: thesis: Sum (r (*) L) = r * (Sum L)

per cases ( r = 0 or r <> 0 ) ;

suppose r = 0 ; :: thesis: Sum (r (*) L) = r * (Sum L)

then ( r (*) L = ZeroLC V & r * (Sum L) = 0. V ) by Def2, RLVECT_1:10;
hence Sum (r (*) L) = r * (Sum L) by RLVECT_2:30; :: thesis: verum

end;

suppose A4: r <> 0 ; :: thesis: Sum (r (*) L) = r * (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 (r (*) L) = r * (Sum L)

hence Sum (r (*) L) = r * (Sum L) by A2; :: thesis: verum

end;

suppose A5: card (Carrier L) = n + 1 ; :: thesis: Sum (r (*) L) = r * (Sum L)

then Carrier L <> {} ;
then consider p being object such that
A6: p in Carrier L by XBOOLE_0:def 1;
reconsider p = p as Element of V by A6;
A7: card ((Carrier L) \ {p}) = n by A5, A6, STIRL2_1:55;
consider Lp being Linear_Combination of {p} such that
A8: Lp . p = L . p by RLVECT_4:37;
set LLp = L - Lp;
(L - Lp) . p = (L . p) - (Lp . p) by RLVECT_2:54
.= 0 by A8 ;
then A9: not p in Carrier (L - Lp) by RLVECT_2:19;
A10: Carrier Lp c= {p} by RLVECT_2:def 6;
then A11: ( Carrier (L - Lp) c= (Carrier L) \/ (Carrier Lp) & (Carrier L) \/ (Carrier Lp) c= (Carrier L) \/ {p} ) by RLVECT_2:55, XBOOLE_1:9;
r * (Carrier Lp) c= {(r * p)}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in r * (Carrier Lp) or x in {(r * p)} )
assume x in r * (Carrier Lp) ; :: thesis: x in {(r * p)}
then consider w being Element of V such that
A12: x = r * w and
A13: w in Carrier Lp ;
w = p by A10, A13, TARSKI:def 1;
hence x in {(r * p)} by A12, TARSKI:def 1; :: thesis: verum

end;

then Carrier (r (*) Lp) c= {(r * p)} by A4, Th23;
then r (*) Lp is Linear_Combination of {(r * p)} by RLVECT_2:def 6;
then A14: Sum (r (*) Lp) = ((r (*) Lp) . (r * p)) * (r * p) by RLVECT_2:32
.= (Lp . ((r ") * (r * p))) * (r * p) by A4, Def2
.= (Lp . (((r ") * r) * p)) * (r * p) by RLVECT_1:def 7
.= (Lp . (1 * p)) * (r * p) by A4, XCMPLX_0:def 7
.= (Lp . p) * (r * p) by RLVECT_1:def 8 ;
A15: (L - Lp) + Lp = L + (Lp - Lp) by RLVECT_2:40
.= L + (ZeroLC V) by RLVECT_2:57
.= L by RLVECT_2:41 ;
then A16: Sum L = (Sum (L - Lp)) + (Sum Lp) by RLVECT_3:1
.= (Sum (L - Lp)) + ((Lp . p) * p) by RLVECT_2:32 ;
(Carrier L) \/ {p} = Carrier L by A6, ZFMISC_1:40;
then Carrier (L - Lp) c= Carrier L by A11;
then card (Carrier (L - Lp)) <= n by A9, A7, NAT_1:43, ZFMISC_1:34;
then A17: Sum (r (*) (L - Lp)) = r * (Sum (L - Lp)) by A2;
r (*) L = (r (*) (L - Lp)) + (r (*) Lp) by A15, Th24;
hence Sum (r (*) L) = (Sum (r (*) (L - Lp))) + (Sum (r (*) Lp)) by RLVECT_3:1
.= (r * (Sum (L - Lp))) + (((Lp . p) * r) * p) by A14, A17, RLVECT_1:def 7
.= (r * (Sum (L - Lp))) + (r * ((Lp . p) * p)) by RLVECT_1:def 7
.= r * (Sum L) by A16, RLVECT_1:def 5 ;
:: thesis: verum

end;

end;

end;

end;

end;

A18: S₁[ 0 ]

proof

let L be Linear_Combination of V; :: thesis: ( card (Carrier L) <= 0 implies Sum (r (*) L) = r * (Sum L) )
assume card (Carrier L) <= 0 ; :: thesis: Sum (r (*) L) = r * (Sum L)
then Carrier L = {} ;
then A19: L = ZeroLC V by RLVECT_2:def 5;
then ( r * (0. V) = 0. V & Sum L = 0. V ) by RLVECT_2:30;
hence Sum (r (*) L) = r * (Sum L) by A19, Th26; :: thesis: verum

end;

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