let GF be Field; :: thesis: for V being VectSp of GF

for L being Linear_Combination of V

for a being Element of GF holds Sum (a * L) = a * (Sum L)

let V be VectSp of GF; :: thesis: for L being Linear_Combination of V

for a being Element of GF holds Sum (a * L) = a * (Sum L)

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

let a be Element of GF; :: thesis: Sum (a * L) = a * (Sum L)

for L being Linear_Combination of V

for a being Element of GF holds Sum (a * L) = a * (Sum L)

let V be VectSp of GF; :: thesis: for L being Linear_Combination of V

for a being Element of GF holds Sum (a * L) = a * (Sum L)

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

let a be Element of GF; :: thesis: Sum (a * L) = a * (Sum L)

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

end;

suppose A1:
a <> 0. GF
; :: 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 Def6;

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 Def6;

A8: len G = len F by A1, A2, A3, A5, A6, Th29, FINSEQ_1:48;

set f = (a * L) (#) F;

set g = L (#) G;

deffunc H_{1}( 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 = H_{1}(k)
from FINSEQ_1:sch 2();

A11: Carrier (a * L) = Carrier L by A1, Th29;

A12: rng P c= Seg (len F)

Seg (len F) c= rng P

A26: dom P = Seg (len F) by A9, FINSEQ_1:def 3;

then A27: P is one-to-one by A25, FINSEQ_4:60;

reconsider P = P as Function of (Seg (len F)),(Seg (len F)) by A12, A26, FUNCT_2:2;

reconsider P = P as Permutation of (Seg (len F)) by A25, A27, FUNCT_2:57;

A28: len ((a * L) (#) F) = len F by Def5;

then dom ((a * L) (#) F) = Seg (len F) by FINSEQ_1:def 3;

then reconsider P = P as Permutation of (dom ((a * L) (#) F)) ;

reconsider Fp = ((a * L) (#) F) * P as FinSequence of the carrier of V by FINSEQ_2:47;

A29: len Fp = len ((a * L) (#) F) by FINSEQ_2:44;

then A30: len Fp = len (L (#) G) by A8, A28, Def5;

hence Sum (a * L) = a * (Sum L) by A4, A7, A30, A31, RLVECT_2:66; :: thesis: verum

end;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 Def6;

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 Def6;

A8: len G = len F by A1, A2, A3, A5, A6, Th29, FINSEQ_1:48;

set f = (a * L) (#) F;

set g = L (#) G;

deffunc H

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 = H

A11: Carrier (a * L) = Carrier L by A1, Th29;

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 A13, FINSEQ_3:23;

y in Seg (len F) by A9, A13, FINSEQ_1:def 3;

then y in dom G by A8, FINSEQ_1:def 3;

then G . y in rng F by A3, A6, A11, FUNCT_1:def 3;

then A15: F just_once_values G . y by A2, FINSEQ_4:8;

P . y = F <- (G . y) by A10, A13;

then P . y in dom F by A15, FINSEQ_4:def 3;

hence x in Seg (len F) by A14, FINSEQ_1:def 3; :: thesis: verum

end;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 A13, FINSEQ_3:23;

y in Seg (len F) by A9, A13, FINSEQ_1:def 3;

then y in dom G by A8, FINSEQ_1:def 3;

then G . y in rng F by A3, A6, A11, FUNCT_1:def 3;

then A15: F just_once_values G . y by A2, FINSEQ_4:8;

P . y = F <- (G . y) by A10, A13;

then P . y in dom F by A15, FINSEQ_4:def 3;

hence x in Seg (len F) by A14, FINSEQ_1:def 3; :: thesis: verum

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 ) )

A18:
dom P = Seg (len F)
by A9, FINSEQ_1:def 3;( ( 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 )

A17: x in dom P and

P . x in dom F ; :: thesis: x in dom G

x in Seg (len P) by A17, FINSEQ_1:def 3;

hence x in dom G by A9, A8, FINSEQ_1:def 3; :: thesis: verum

end;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 that
assume
x in dom G
; :: thesis: ( x in dom P & P . x in dom F )

then x in Seg (len P) by A9, A8, 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 3;

then P . x in Seg (len F) by A12;

hence P . x in dom F by FINSEQ_1:def 3; :: thesis: verum

end;then x in Seg (len P) by A9, A8, 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 3;

then P . x in Seg (len F) by A12;

hence P . x in dom F by FINSEQ_1:def 3; :: thesis: verum

A17: x in dom P and

P . x in dom F ; :: thesis: x in dom G

x in Seg (len P) by A17, FINSEQ_1:def 3;

hence x in dom G by A9, A8, FINSEQ_1:def 3; :: thesis: verum

now :: thesis: for x being object st x in dom G holds

G . x = F . (P . x)

then A21:
G = F * P
by A16, FUNCT_1:10;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 A3, A6, A11, A19, FUNCT_1:def 3;

then A20: F just_once_values G . n by A2, FINSEQ_4:8;

n in Seg (len F) by A8, A19, FINSEQ_1:def 3;

then F . (P . n) = F . (F <- (G . n)) by A10, A18

.= G . n by A20, FINSEQ_4:def 3 ;

hence G . x = F . (P . x) ; :: thesis: verum

end;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 A3, A6, A11, A19, FUNCT_1:def 3;

then A20: F just_once_values G . n by A2, FINSEQ_4:8;

n in Seg (len F) by A8, A19, FINSEQ_1:def 3;

then F . (P . n) = F . (F <- (G . n)) by A10, A18

.= G . n by A20, FINSEQ_4:def 3 ;

hence G . x = F . (P . x) ; :: thesis: verum

Seg (len F) c= rng P

proof

then A25:
Seg (len F) = rng P
by A12;
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 A2, A3, A6, A11, FUNCT_1:33;

then A23: rng ((F ") * G) = rng (F ") by RELAT_1:28

.= dom F by A2, FUNCT_1:33 ;

A24: rng P c= dom F by A12, FINSEQ_1:def 3;

(F ") * G = ((F ") * F) * P by A21, RELAT_1:36

.= (id (dom F)) * P by A2, FUNCT_1:39

.= P by A24, RELAT_1:53 ;

hence x in rng P by A22, A23, FINSEQ_1:def 3; :: thesis: verum

end;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 A2, A3, A6, A11, FUNCT_1:33;

then A23: rng ((F ") * G) = rng (F ") by RELAT_1:28

.= dom F by A2, FUNCT_1:33 ;

A24: rng P c= dom F by A12, FINSEQ_1:def 3;

(F ") * G = ((F ") * F) * P by A21, RELAT_1:36

.= (id (dom F)) * P by A2, FUNCT_1:39

.= P by A24, RELAT_1:53 ;

hence x in rng P by A22, A23, FINSEQ_1:def 3; :: thesis: verum

A26: dom P = Seg (len F) by A9, FINSEQ_1:def 3;

then A27: P is one-to-one by A25, FINSEQ_4:60;

reconsider P = P as Function of (Seg (len F)),(Seg (len F)) by A12, A26, FUNCT_2:2;

reconsider P = P as Permutation of (Seg (len F)) by A25, A27, FUNCT_2:57;

A28: len ((a * L) (#) F) = len F by Def5;

then dom ((a * L) (#) F) = Seg (len F) by FINSEQ_1:def 3;

then reconsider P = P as Permutation of (dom ((a * L) (#) F)) ;

reconsider Fp = ((a * L) (#) F) * P as FinSequence of the carrier of V by FINSEQ_2:47;

A29: len Fp = len ((a * L) (#) F) by FINSEQ_2:44;

then A30: len Fp = len (L (#) G) by A8, A28, Def5;

A31: 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

( Sum Fp = Sum ((a * L) (#) F) & dom Fp = dom (L (#) G) )
by A30, FINSEQ_3:29, RLVECT_2:7;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

A32: k in dom (L (#) G) and

A33: v = (L (#) G) . k ; :: thesis: Fp . k = a * v

A34: k in Seg (len (L (#) G)) by A32, FINSEQ_1:def 3;

then A35: k in dom P by A9, A28, A29, A30, FINSEQ_1:def 3;

A36: k in dom G by A8, A28, A29, A30, A34, FINSEQ_1:def 3;

then G . k in rng G by FUNCT_1:def 3;

then F just_once_values G . k by A2, A3, A6, A11, FINSEQ_4:8;

then A37: 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;

A38: G /. k = G . k by A36, PARTFUN1:def 6

.= F . (P . k) by A21, A35, FUNCT_1:13

.= F . i by A10, A18, A28, A29, A30, A34

.= F /. i by A37, PARTFUN1:def 6 ;

i in Seg (len ((a * L) (#) F)) by A28, A37, FINSEQ_1:def 3;

then A39: i in dom ((a * L) (#) F) by FINSEQ_1:def 3;

thus Fp . k = ((a * L) (#) F) . (P . k) by A35, FUNCT_1:13

.= ((a * L) (#) F) . (F <- (G . k)) by A10, A18, A28, A29, A30, A34

.= ((a * L) . (F /. i)) * (F /. i) by A39, Def5

.= (a * (L . (F /. i))) * (F /. i) by Def9

.= a * ((L . (F /. i)) * (F /. i)) by VECTSP_1:def 16

.= a * v by A32, A33, A38, Def5 ; :: thesis: verum

end;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

A32: k in dom (L (#) G) and

A33: v = (L (#) G) . k ; :: thesis: Fp . k = a * v

A34: k in Seg (len (L (#) G)) by A32, FINSEQ_1:def 3;

then A35: k in dom P by A9, A28, A29, A30, FINSEQ_1:def 3;

A36: k in dom G by A8, A28, A29, A30, A34, FINSEQ_1:def 3;

then G . k in rng G by FUNCT_1:def 3;

then F just_once_values G . k by A2, A3, A6, A11, FINSEQ_4:8;

then A37: 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;

A38: G /. k = G . k by A36, PARTFUN1:def 6

.= F . (P . k) by A21, A35, FUNCT_1:13

.= F . i by A10, A18, A28, A29, A30, A34

.= F /. i by A37, PARTFUN1:def 6 ;

i in Seg (len ((a * L) (#) F)) by A28, A37, FINSEQ_1:def 3;

then A39: i in dom ((a * L) (#) F) by FINSEQ_1:def 3;

thus Fp . k = ((a * L) (#) F) . (P . k) by A35, FUNCT_1:13

.= ((a * L) (#) F) . (F <- (G . k)) by A10, A18, A28, A29, A30, A34

.= ((a * L) . (F /. i)) * (F /. i) by A39, Def5

.= (a * (L . (F /. i))) * (F /. i) by Def9

.= a * ((L . (F /. i)) * (F /. i)) by VECTSP_1:def 16

.= a * v by A32, A33, A38, Def5 ; :: thesis: verum

hence Sum (a * L) = a * (Sum L) by A4, A7, A30, A31, RLVECT_2:66; :: thesis: verum