let a be Real; :: thesis: for V being RealLinearSpace
for L being Linear_Combination of V holds Sum (a * L) = a * (Sum L)
let V be RealLinearSpace; :: thesis: for L being Linear_Combination of V holds Sum (a * L) = a * (Sum L)
let L be Linear_Combination of V; :: thesis: Sum (a * L) = a * (Sum L)

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

suppose A1: a <> 0 ; :: thesis: Sum (a * L) = a * (Sum L)

consider F being FinSequence of the carrier of V such that
A2: F is one-to-one and
A3: rng F = Carrier (a * L) and
A4: Sum (a * L) = Sum ((a * L) (#) F) by RLVECT_2:def 10;
consider G being FinSequence of the carrier of V such that
A5: G is one-to-one and
A6: rng G = Carrier L and
A7: Sum L = Sum (L (#) G) by RLVECT_2:def 10;
set g = L (#) G;
set f = (a * L) (#) F;
set l = a * L;
deffunc H₁( Nat) -> set = F <- (G . $1);
consider P being FinSequence such that
A8: len P = len F and
A9: for k being Nat st k in dom P holds
P . k = H₁(k) from FINSEQ_1:sch 2();
A10: dom P = Seg (len F) by A8, FINSEQ_1:def 3;
A11: Carrier (a * L) = Carrier L by A1, RLVECT_2:65;
A12: len G = len F by A1, A2, A3, A5, A6, FINSEQ_1:65, RLVECT_2:65;
A13: rng P c= Seg (len F)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng P or x in Seg (len F) )
assume x in rng P ; :: thesis: x in Seg (len F)
then consider y being set such that
A14: y in dom P and
A15: P . y = x by FUNCT_1:def 5;
reconsider y = y as Element of NAT by A14, FINSEQ_3:25;
A16: y in Seg (len F) by A8, A14, FINSEQ_1:def 3;
then y in dom G by A12, FINSEQ_1:def 3;
then G . y in rng F by A3, A6, A11, FUNCT_1:def 5;
then ( P . y = F <- (G . y) & F just_once_values G . y ) by A2, A9, A16, A10, FINSEQ_4:10;
then P . y in dom F by FINSEQ_4:def 3;
hence x in Seg (len F) by A15, FINSEQ_1:def 3; :: thesis: verum

end;

A17: now

let x be set ; :: thesis: ( ( x in dom G implies ( x in dom P & P . x in dom F ) ) & ( x in dom P & P . x in dom F implies x in dom G ) )
thus ( x in dom G implies ( x in dom P & P . x in dom F ) ) :: thesis: ( x in dom P & P . x in dom F implies x in dom G )

proof

assume x in dom G ; :: thesis: ( x in dom P & P . x in dom F )
then x in Seg (len P) by A8, A12, FINSEQ_1:def 3;
hence x in dom P by FINSEQ_1:def 3; :: thesis: P . x in dom F
then ( rng P c= Seg (len F) & P . x in rng P ) by A13, FUNCT_1:def 5;
then P . x in Seg (len F) ;
hence P . x in dom F by FINSEQ_1:def 3; :: thesis: verum

end;

assume ( x in dom P & P . x in dom F ) ; :: thesis: x in dom G
then x in Seg (len P) by FINSEQ_1:def 3;
hence x in dom G by A8, A12, FINSEQ_1:def 3; :: thesis: verum

end;

now

let x be set ; :: thesis: ( x in dom G implies G . x = F . (P . x) )
assume A18: x in dom G ; :: thesis: G . x = F . (P . x)
then reconsider n = x as Element of NAT by FINSEQ_3:25;
G . n in rng F by A3, A6, A11, A18, FUNCT_1:def 5;
then A19: F just_once_values G . n by A2, FINSEQ_4:10;
n in Seg (len F) by A12, A18, FINSEQ_1:def 3;
then F . (P . n) = F . (F <- (G . n)) by A9, A10
.= G . n by A19, FINSEQ_4:def 3 ;
hence G . x = F . (P . x) ; :: thesis: verum

end;

then A20: G = F * P by A17, FUNCT_1:20;
Seg (len F) c= rng P

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Seg (len F) or x in rng P )
assume A21: x in Seg (len F) ; :: thesis: x in rng P
set f = (F " ) * G;
dom (F " ) = rng G by A2, A3, A6, A11, FUNCT_1:55;
then A22: rng ((F " ) * G) = rng (F " ) by RELAT_1:47
.= dom F by A2, FUNCT_1:55 ;
A23: rng P c= dom F by A13, FINSEQ_1:def 3;
(F " ) * G = ((F " ) * F) * P by A20, RELAT_1:55
.= (id (dom F)) * P by A2, FUNCT_1:61
.= P by A23, RELAT_1:79 ;
hence x in rng P by A21, A22, FINSEQ_1:def 3; :: thesis: verum

end;

then A24: Seg (len F) = rng P by A13, XBOOLE_0:def 10;
A25: dom P = Seg (len F) by A8, FINSEQ_1:def 3;
then A26: P is one-to-one by A24, FINSEQ_4:75;
( Seg (len F) = {} implies Seg (len F) = {} ) ;
then reconsider P = P as Function of (Seg (len F)),(Seg (len F)) by A13, A25, FUNCT_2:def 1, RELSET_1:11;
reconsider P = P as Permutation of (Seg (len F)) by A24, A26, FUNCT_2:83;
A27: len ((a * L) (#) F) = len F by RLVECT_2:def 9;
then A28: dom ((a * L) (#) F) = Seg (len F) by FINSEQ_1:def 3;
then reconsider Fp = ((a * L) (#) F) * P as FinSequence of the carrier of V by FINSEQ_2:51;
dom ((a * L) (#) F) = Seg (len ((a * L) (#) F)) by FINSEQ_1:def 3;
then A29: Sum Fp = Sum ((a * L) (#) F) by A27, RLVECT_2:9;
A30: len Fp = len ((a * L) (#) F) by A28, FINSEQ_2:48;
then A31: len Fp = len (L (#) G) by A12, A27, RLVECT_2:def 9;
then A32: dom Fp = dom (L (#) G) by FINSEQ_3:31;

now

let k be Element of NAT ; :: thesis: for v being VECTOR of V st k in dom (L (#) G) & v = (L (#) G) . k holds
Fp . k = a * v
let v be VECTOR of V; :: thesis: ( k in dom (L (#) G) & v = (L (#) G) . k implies Fp . k = a * v )
assume that
A33: k in dom (L (#) G) and
A34: v = (L (#) G) . k ; :: thesis: Fp . k = a * v
A35: k in dom G by A12, A27, A30, A31, A33, FINSEQ_3:31;
then G . k in rng G by FUNCT_1:def 5;
then F just_once_values G . k by A2, A3, A6, A11, FINSEQ_4:10;
then A36: F <- (G . k) in dom F by FINSEQ_4:def 3;
then reconsider i = F <- (G . k) as Element of NAT by FINSEQ_3:25;
A37: k in Seg (len F) by A27, A30, A31, A33, FINSEQ_1:def 3;
A38: k in dom P by A8, A27, A30, A31, A33, FINSEQ_3:31;
A39: G /. k = G . k by A35, PARTFUN1:def 8
.= F . (P . k) by A20, A38, FUNCT_1:23
.= F . i by A9, A37, A10
.= F /. i by A36, PARTFUN1:def 8 ;
i in Seg (len ((a * L) (#) F)) by A27, A36, FINSEQ_1:def 3;
then A40: i in dom ((a * L) (#) F) by FINSEQ_1:def 3;
thus Fp . k = ((a * L) (#) F) . (P . k) by A38, FUNCT_1:23
.= ((a * L) (#) F) . (F <- (G . k)) by A9, A37, A10
.= ((a * L) . (F /. i)) * (F /. i) by A40, RLVECT_2:def 9
.= (a * (L . (F /. i))) * (F /. i) by RLVECT_2:def 13
.= a * ((L . (F /. i)) * (F /. i)) by RLVECT_1:def 9
.= a * v by A33, A34, A39, RLVECT_2:def 9 ; :: thesis: verum

end;

hence Sum (a * L) = a * (Sum L) by A4, A7, A29, A31, A32, RLVECT_1:56; :: thesis: verum

end;

suppose A41: a = 0 ; :: thesis: Sum (a * L) = a * (Sum L)

hence Sum (a * L) = Sum (ZeroLC V) by RLVECT_2:66
.= 0. V by RLVECT_2:48
.= a * (Sum L) by A41, RLVECT_1:23 ;
:: thesis: verum

end;

end;