let R be domRing; :: thesis: for V being RightMod of R
for L being Linear_Combination of V
for a being Scalar of R holds Sum (L * a) = (Sum L) * a
let V be RightMod of R; :: thesis: for L being Linear_Combination of V
for a being Scalar of R holds Sum (L * a) = (Sum L) * a
let L be Linear_Combination of V; :: thesis: for a being Scalar of R holds Sum (L * a) = (Sum L) * a
let a be Scalar of R; :: thesis: Sum (L * a) = (Sum L) * a

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

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

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

A13: now

let x be set ; :: thesis: ( x in dom G implies G . x = F . (P . x) )
assume A14: x in dom G ; :: thesis: G . x = F . (P . x)
then reconsider n = x as Nat by FINSEQ_3:25;
G . n in rng F by A7, A4, A2, A14, FUNCT_1:def 5;
then A15: F just_once_values G . n by A6, FINSEQ_4:10;
n in Seg (len F) by A9, A14, FINSEQ_1:def 3;
then F . (P . n) = F . (F <- (G . n)) by A11, A12
.= G . n by A15, FINSEQ_4:def 3 ;
hence G . x = F . (P . x) ; :: thesis: verum

end;

A16: rng P c= dom F

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng P or x in dom F )
assume x in rng P ; :: thesis: x in dom F
then consider y being set such that
A17: y in dom P and
A18: P . y = x by FUNCT_1:def 5;
reconsider y = y as Nat by A17, FINSEQ_3:25;
y in dom G by A10, A9, A17, FINSEQ_3:31;
then G . y in rng F by A7, A4, A2, FUNCT_1:def 5;
then A19: F just_once_values G . y by A6, FINSEQ_4:10;
P . y = F <- (G . y) by A11, A17;
hence x in dom F by A18, A19, FINSEQ_4:def 3; :: thesis: verum

end;

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 A10, A9, FINSEQ_1:def 3;
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 5;
hence P . x in dom F by A16; :: thesis: verum

end;

assume that
A20: x in dom P and
P . x in dom F ; :: thesis: x in dom G
x in Seg (len P) by A20, FINSEQ_1:def 3;
hence x in dom G by A10, A9, FINSEQ_1:def 3; :: thesis: verum

end;

then A21: G = F * P by A13, FUNCT_1:20;
dom F c= rng P

proof

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

end;

then A24: dom F = rng P by A16, XBOOLE_0:def 10;
A25: dom P = dom F by A10, FINSEQ_3:31;
then A26: P is one-to-one by A24, FINSEQ_4:75;
( dom F = {} implies dom F = {} ) ;
then reconsider P = P as Function of (dom F),(dom F) by A16, A25, FUNCT_2:def 1, RELSET_1:11;
A27: len ((L * a) (#) F) = len F by Def8;
then A28: dom ((L * a) (#) F) = dom F by FINSEQ_3:31;
then reconsider P = P as Function of (dom ((L * a) (#) F)),(dom ((L * a) (#) F)) ;
reconsider Fp = ((L * a) (#) F) * P as FinSequence of V by FINSEQ_2:51;
reconsider P = P as Permutation of (dom ((L * a) (#) F)) by A24, A26, A28, FUNCT_2:83;
A29: Fp = ((L * a) (#) F) * P ;
then A30: len Fp = len ((L * a) (#) F) by FINSEQ_2:48;
then A31: len Fp = len (L (#) G) by A9, A27, Def8;

A32: now

let k be Nat; :: thesis: for v being Vector of V st k in dom Fp & v = (L (#) G) . k holds
Fp . k = v * a
let v be Vector of V; :: thesis: ( k in dom Fp & v = (L (#) G) . k implies Fp . k = v * a )
assume that
A33: k in dom Fp and
A34: v = (L (#) G) . k ; :: thesis: Fp . k = v * a
A35: k in Seg (len (L (#) G)) by A31, A33, FINSEQ_1:def 3;
then A36: k in dom P by A10, A27, A30, A31, FINSEQ_1:def 3;
A37: k in dom G by A9, A27, A30, A31, A35, FINSEQ_1:def 3;
then G . k in rng G by FUNCT_1:def 5;
then F just_once_values G . k by A6, A7, A4, A2, FINSEQ_4:10;
then A38: F <- (G . k) in dom F by FINSEQ_4:def 3;
then reconsider i = F <- (G . k) as Nat by FINSEQ_3:25;
A39: G /. k = G . k by A37, PARTFUN1:def 8
.= F . (P . k) by A21, A36, FUNCT_1:23
.= F . i by A11, A12, A27, A30, A31, A35
.= F /. i by A38, PARTFUN1:def 8 ;
A40: k in dom (L (#) G) by A35, FINSEQ_1:def 3;
i in Seg (len ((L * a) (#) F)) by A27, A38, FINSEQ_1:def 3;
then A41: i in dom ((L * a) (#) F) by FINSEQ_1:def 3;
thus Fp . k = ((L * a) (#) F) . (P . k) by A36, FUNCT_1:23
.= ((L * a) (#) F) . (F <- (G . k)) by A11, A12, A27, A30, A31, A35
.= (F /. i) * ((L * a) . (F /. i)) by A41, Def8
.= (F /. i) * ((L . (F /. i)) * a) by Def12
.= ((F /. i) * (L . (F /. i))) * a by VECTSP_2:def 23
.= v * a by A34, A40, A39, Def8 ; :: thesis: verum

end;

Sum Fp = Sum ((L * a) (#) F) by A29, RLVECT_2:9;
hence Sum (L * a) = (Sum L) * a by A8, A5, A31, A32, Th1; :: thesis: verum

end;

suppose A42: a = 0. R ; :: thesis: Sum (L * a) = (Sum L) * a

hence Sum (L * a) = Sum (ZeroLC V) by Th60
.= 0. V by Lm3
.= (Sum L) * a by A42, VECTSP_2:90 ;
:: thesis: verum

end;

end;