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)
set l = a * 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 8;
set f = (a * L) (#) F;
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 8;
A8: len G = len F by ;
deffunc H1( Nat) -> set = F <- (G . \$1);
consider P being FinSequence such that
A9: len P = len F and
A10: for k being Nat st k in dom P holds
P . k = H1(k) from A11: Carrier (a * L) = Carrier L by ;
A12: rng P c= Seg (len F)
proof
let x be object ; :: 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 object such that
A13: y in dom P and
A14: P . y = x by FUNCT_1:def 3;
reconsider y = y as Element of NAT by ;
y in Seg (len F) by ;
then y in dom G by ;
then G . y in rng F by ;
then A15: F just_once_values G . y by ;
P . y = F <- (G . y) by ;
then P . y in dom F by ;
hence x in Seg (len F) by ; :: thesis: verum
end;
A16: now :: thesis: for x being object holds
( ( 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 ) )
let x be object ; :: 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 ;
hence x in dom P by FINSEQ_1:def 3; :: thesis: P . x in dom F
then P . x in rng P by FUNCT_1:def 3;
then P . x in Seg (len F) by A12;
hence P . x in dom F by FINSEQ_1:def 3; :: thesis: verum
end;
assume that
A17: x in dom P and
P . x in dom F ; :: thesis: x in dom G
x in Seg (len P) by ;
hence x in dom G by ; :: thesis: verum
end;
A18: dom P = Seg (len F) by ;
now :: thesis: for x being object st x in dom G holds
G . x = F . (P . x)
let x be object ; :: thesis: ( x in dom G implies G . x = F . (P . x) )
assume A19: x in dom G ; :: thesis: G . x = F . (P . x)
then reconsider n = x as Element of NAT by FINSEQ_3:23;
G . n in rng F by ;
then A20: F just_once_values G . n by ;
n in Seg (len F) by ;
then F . (P . n) = F . (F <- (G . n)) by
.= G . n by ;
hence G . x = F . (P . x) ; :: thesis: verum
end;
then A21: G = F * P by ;
Seg (len F) c= rng P
proof
set f = (F ") * G;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Seg (len F) or x in rng P )
assume A22: x in Seg (len F) ; :: thesis: x in rng P
dom (F ") = rng G by ;
then A23: rng ((F ") * G) = rng (F ") by RELAT_1:28
.= dom F by ;
A24: rng P c= dom F by ;
(F ") * G = ((F ") * F) * P by
.= (id (dom F)) * P by
.= P by ;
hence x in rng P by ; :: thesis: verum
end;
then A25: Seg (len F) = rng P by A12;
A26: dom P = Seg (len F) by ;
then A27: P is one-to-one by ;
reconsider P = P as Function of (Seg (len F)),(Seg (len F)) by ;
reconsider P = P as Permutation of (Seg (len F)) by ;
A28: len ((a * L) (#) F) = len F by RLVECT_2:def 7;
then A29: 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:47;
set g = L (#) G;
dom ((a * L) (#) F) = Seg (len ((a * L) (#) F)) by FINSEQ_1:def 3;
then A30: Sum Fp = Sum ((a * L) (#) F) by ;
A31: len Fp = len ((a * L) (#) F) by ;
then A32: len Fp = len (L (#) G) by ;
A33: now :: thesis: for k being Nat
for v being VECTOR of V st k in dom (L (#) G) & v = (L (#) G) . k holds
Fp . k = a * v
let k be 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
A34: k in dom (L (#) G) and
A35: v = (L (#) G) . k ; :: thesis: Fp . k = a * v
A36: k in Seg (len F) by ;
A37: k in dom G by ;
then G . k in rng G by FUNCT_1:def 3;
then F just_once_values G . k by ;
then A38: F <- (G . k) in dom F by FINSEQ_4:def 3;
then reconsider i = F <- (G . k) as Element of NAT by FINSEQ_3:23;
i in Seg (len ((a * L) (#) F)) by ;
then A39: i in dom ((a * L) (#) F) by FINSEQ_1:def 3;
A40: k in dom P by ;
A41: G /. k = G . k by
.= F . (P . k) by
.= F . i by
.= F /. i by ;
thus Fp . k = ((a * L) (#) F) . (P . k) by
.= ((a * L) (#) F) . (F <- (G . k)) by
.= ((a * L) . (F /. i)) * (F /. i) by
.= (a * (L . (F /. i))) * (F /. i) by RLVECT_2:def 11
.= a * ((L . (F /. i)) * (F /. i)) by RLVECT_1:def 7
.= a * v by ; :: thesis: verum
end;
dom Fp = dom (L (#) G) by ;
hence Sum (a * L) = a * (Sum L) by ; :: thesis: verum
end;
suppose A42: a = 0 ; :: thesis: Sum (a * L) = a * (Sum L)
hence Sum (a * L) = Sum () by RLVECT_2:43
.= 0. V by RLVECT_2:30
.= a * (Sum L) by ;
:: thesis: verum
end;
end;