let K be Ring; :: thesis: for V being LeftMod of K

for L being Function of the carrier of V, the carrier of K

for A being Subset of V

for F, F1 being FinSequence of the carrier of V st F is one-to-one & rng F = A & F1 is one-to-one & rng F1 = A holds

Sum (L (#) F) = Sum (L (#) F1)

let V be LeftMod of K; :: thesis: for L being Function of the carrier of V, the carrier of K

for A being Subset of V

for F, F1 being FinSequence of the carrier of V st F is one-to-one & rng F = A & F1 is one-to-one & rng F1 = A holds

Sum (L (#) F) = Sum (L (#) F1)

let L be Function of the carrier of V, the carrier of K; :: thesis: for A being Subset of V

for F, F1 being FinSequence of the carrier of V st F is one-to-one & rng F = A & F1 is one-to-one & rng F1 = A holds

Sum (L (#) F) = Sum (L (#) F1)

let A be Subset of V; :: thesis: for F, F1 being FinSequence of the carrier of V st F is one-to-one & rng F = A & F1 is one-to-one & rng F1 = A holds

Sum (L (#) F) = Sum (L (#) F1)

let F, F1 be FinSequence of the carrier of V; :: thesis: ( F is one-to-one & rng F = A & F1 is one-to-one & rng F1 = A implies Sum (L (#) F) = Sum (L (#) F1) )

assume that

A4: F is one-to-one and

A5: rng F = A and

A7: F1 is one-to-one and

A8: rng F1 = A ; :: thesis: Sum (L (#) F) = Sum (L (#) F1)

set v1 = Sum (L (#) F);

set v2 = Sum (L (#) F1);

defpred S_{1}[ object , object ] means {$2} = F " {(F1 . $1)};

A10: len F = len F1 by A4, A5, A7, A8, FINSEQ_1:48;

A11: dom F = Seg (len F) by FINSEQ_1:def 3;

A12: dom F1 = Seg (len F1) by FINSEQ_1:def 3;

A13: for x being object st x in dom F holds

ex y being object st

( y in dom F & S_{1}[x,y] )

A15: for x being object st x in dom F holds

S_{1}[x,f . x]
from FUNCT_2:sch 1(A13);

A16: rng f = dom F

A21: len G1 = len F by VECTSP_6:def 5;

A22: f is one-to-one

A33: dom (L (#) F1) = Seg (len (L (#) F1)) by FINSEQ_1:def 3;

reconsider f = f as Permutation of (dom F) by A16, A22, FUNCT_2:57;

( dom F = Seg (len F) & dom G1 = Seg (len G1) ) by FINSEQ_1:def 3;

then reconsider f = f as Permutation of (dom G1) by A21;

A34: len (L (#) F1) = len F1 by VECTSP_6:def 5;

A35: dom G1 = Seg (len G1) by FINSEQ_1:def 3;

for L being Function of the carrier of V, the carrier of K

for A being Subset of V

for F, F1 being FinSequence of the carrier of V st F is one-to-one & rng F = A & F1 is one-to-one & rng F1 = A holds

Sum (L (#) F) = Sum (L (#) F1)

let V be LeftMod of K; :: thesis: for L being Function of the carrier of V, the carrier of K

for A being Subset of V

for F, F1 being FinSequence of the carrier of V st F is one-to-one & rng F = A & F1 is one-to-one & rng F1 = A holds

Sum (L (#) F) = Sum (L (#) F1)

let L be Function of the carrier of V, the carrier of K; :: thesis: for A being Subset of V

for F, F1 being FinSequence of the carrier of V st F is one-to-one & rng F = A & F1 is one-to-one & rng F1 = A holds

Sum (L (#) F) = Sum (L (#) F1)

let A be Subset of V; :: thesis: for F, F1 being FinSequence of the carrier of V st F is one-to-one & rng F = A & F1 is one-to-one & rng F1 = A holds

Sum (L (#) F) = Sum (L (#) F1)

let F, F1 be FinSequence of the carrier of V; :: thesis: ( F is one-to-one & rng F = A & F1 is one-to-one & rng F1 = A implies Sum (L (#) F) = Sum (L (#) F1) )

assume that

A4: F is one-to-one and

A5: rng F = A and

A7: F1 is one-to-one and

A8: rng F1 = A ; :: thesis: Sum (L (#) F) = Sum (L (#) F1)

set v1 = Sum (L (#) F);

set v2 = Sum (L (#) F1);

defpred S

A10: len F = len F1 by A4, A5, A7, A8, FINSEQ_1:48;

A11: dom F = Seg (len F) by FINSEQ_1:def 3;

A12: dom F1 = Seg (len F1) by FINSEQ_1:def 3;

A13: for x being object st x in dom F holds

ex y being object st

( y in dom F & S

proof

consider f being Function of (dom F),(dom F) such that
let x be object ; :: thesis: ( x in dom F implies ex y being object st

( y in dom F & S_{1}[x,y] ) )

assume x in dom F ; :: thesis: ex y being object st

( y in dom F & S_{1}[x,y] )

then F1 . x in rng F by A5, A8, A10, A11, A12, FUNCT_1:def 3;

then consider y being object such that

A14: F " {(F1 . x)} = {y} by A4, FUNCT_1:74;

take y ; :: thesis: ( y in dom F & S_{1}[x,y] )

y in F " {(F1 . x)} by A14, TARSKI:def 1;

hence y in dom F by FUNCT_1:def 7; :: thesis: S_{1}[x,y]

thus S_{1}[x,y]
by A14; :: thesis: verum

end;( y in dom F & S

assume x in dom F ; :: thesis: ex y being object st

( y in dom F & S

then F1 . x in rng F by A5, A8, A10, A11, A12, FUNCT_1:def 3;

then consider y being object such that

A14: F " {(F1 . x)} = {y} by A4, FUNCT_1:74;

take y ; :: thesis: ( y in dom F & S

y in F " {(F1 . x)} by A14, TARSKI:def 1;

hence y in dom F by FUNCT_1:def 7; :: thesis: S

thus S

A15: for x being object st x in dom F holds

S

A16: rng f = dom F

proof

reconsider G1 = L (#) F as FinSequence of V ;
thus
rng f c= dom F
; :: according to XBOOLE_0:def 10 :: thesis: dom F c= rng f

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in dom F or y in rng f )

assume A17: y in dom F ; :: thesis: y in rng f

then F . y in rng F1 by A5, A8, FUNCT_1:def 3;

then consider x being object such that

A18: x in dom F1 and

A19: F1 . x = F . y by FUNCT_1:def 3;

F " {(F1 . x)} = F " (Im (F,y)) by A17, A19, FUNCT_1:59;

then F " {(F1 . x)} c= {y} by A4, FUNCT_1:82;

then {(f . x)} c= {y} by A10, A11, A12, A15, A18;

then A20: f . x = y by ZFMISC_1:18;

x in dom f by A10, A11, A12, A18, FUNCT_2:def 1;

hence y in rng f by A20, FUNCT_1:def 3; :: thesis: verum

end;let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in dom F or y in rng f )

assume A17: y in dom F ; :: thesis: y in rng f

then F . y in rng F1 by A5, A8, FUNCT_1:def 3;

then consider x being object such that

A18: x in dom F1 and

A19: F1 . x = F . y by FUNCT_1:def 3;

F " {(F1 . x)} = F " (Im (F,y)) by A17, A19, FUNCT_1:59;

then F " {(F1 . x)} c= {y} by A4, FUNCT_1:82;

then {(f . x)} c= {y} by A10, A11, A12, A15, A18;

then A20: f . x = y by ZFMISC_1:18;

x in dom f by A10, A11, A12, A18, FUNCT_2:def 1;

hence y in rng f by A20, FUNCT_1:def 3; :: thesis: verum

A21: len G1 = len F by VECTSP_6:def 5;

A22: f is one-to-one

proof

set G2 = L (#) F1;
let y1, y2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not y1 in dom f or not y2 in dom f or not f . y1 = f . y2 or y1 = y2 )

assume that

A23: y1 in dom f and

A24: y2 in dom f and

A25: f . y1 = f . y2 ; :: thesis: y1 = y2

A28: F " {(F1 . y2)} = {(f . y2)} by A15, A24;

F1 . y1 in rng F by A5, A8, A10, A11, A12, A23, FUNCT_1:def 3;

then A30: {(F1 . y1)} c= rng F by ZFMISC_1:31;

F1 . y2 in rng F by A5, A8, A10, A11, A12, A24, FUNCT_1:def 3;

then A31: {(F1 . y2)} c= rng F by ZFMISC_1:31;

F " {(F1 . y1)} = {(f . y1)} by A15, A23;

then {(F1 . y1)} = {(F1 . y2)} by A25, A28, A30, A31, FUNCT_1:91;

hence y1 = y2 by A7, A10, A11, A12, A23, A24, ZFMISC_1:3; :: thesis: verum

end;assume that

A23: y1 in dom f and

A24: y2 in dom f and

A25: f . y1 = f . y2 ; :: thesis: y1 = y2

A28: F " {(F1 . y2)} = {(f . y2)} by A15, A24;

F1 . y1 in rng F by A5, A8, A10, A11, A12, A23, FUNCT_1:def 3;

then A30: {(F1 . y1)} c= rng F by ZFMISC_1:31;

F1 . y2 in rng F by A5, A8, A10, A11, A12, A24, FUNCT_1:def 3;

then A31: {(F1 . y2)} c= rng F by ZFMISC_1:31;

F " {(F1 . y1)} = {(f . y1)} by A15, A23;

then {(F1 . y1)} = {(F1 . y2)} by A25, A28, A30, A31, FUNCT_1:91;

hence y1 = y2 by A7, A10, A11, A12, A23, A24, ZFMISC_1:3; :: thesis: verum

A33: dom (L (#) F1) = Seg (len (L (#) F1)) by FINSEQ_1:def 3;

reconsider f = f as Permutation of (dom F) by A16, A22, FUNCT_2:57;

( dom F = Seg (len F) & dom G1 = Seg (len G1) ) by FINSEQ_1:def 3;

then reconsider f = f as Permutation of (dom G1) by A21;

A34: len (L (#) F1) = len F1 by VECTSP_6:def 5;

A35: dom G1 = Seg (len G1) by FINSEQ_1:def 3;

now :: thesis: for i being Nat st i in dom (L (#) F1) holds

(L (#) F1) . i = G1 . (f . i)

hence
Sum (L (#) F) = Sum (L (#) F1)
by A4, A5, A7, A8, A21, A34, FINSEQ_1:48, RLVECT_2:6; :: thesis: verum(L (#) F1) . i = G1 . (f . i)

let i be Nat; :: thesis: ( i in dom (L (#) F1) implies (L (#) F1) . i = G1 . (f . i) )

assume A36: i in dom (L (#) F1) ; :: thesis: (L (#) F1) . i = G1 . (f . i)

then A37: ( (L (#) F1) . i = (L . (F1 /. i)) * (F1 /. i) & F1 . i = F1 /. i ) by A34, A12, A33, VECTSP_6:def 5, PARTFUN1:def 6;

i in dom F1 by A34, A36, FINSEQ_3:29;

then reconsider u = F1 . i as Element of V by FINSEQ_2:11;

i in dom f by A10, A21, A34, A35, A33, A36, FUNCT_2:def 1;

then A38: f . i in dom F by A16, FUNCT_1:def 3;

then reconsider m = f . i as Element of NAT ;

reconsider v = F . m as Element of V by A38, FINSEQ_2:11;

{(F . (f . i))} = Im (F,(f . i)) by A38, FUNCT_1:59

.= F .: (F " {(F1 . i)}) by A10, A34, A11, A33, A15, A36 ;

then A39: u = v by FUNCT_1:75, ZFMISC_1:18;

F . m = F /. m by A38, PARTFUN1:def 6;

hence (L (#) F1) . i = G1 . (f . i) by A21, A11, A35, A38, A39, A37, VECTSP_6:def 5; :: thesis: verum

end;assume A36: i in dom (L (#) F1) ; :: thesis: (L (#) F1) . i = G1 . (f . i)

then A37: ( (L (#) F1) . i = (L . (F1 /. i)) * (F1 /. i) & F1 . i = F1 /. i ) by A34, A12, A33, VECTSP_6:def 5, PARTFUN1:def 6;

i in dom F1 by A34, A36, FINSEQ_3:29;

then reconsider u = F1 . i as Element of V by FINSEQ_2:11;

i in dom f by A10, A21, A34, A35, A33, A36, FUNCT_2:def 1;

then A38: f . i in dom F by A16, FUNCT_1:def 3;

then reconsider m = f . i as Element of NAT ;

reconsider v = F . m as Element of V by A38, FINSEQ_2:11;

{(F . (f . i))} = Im (F,(f . i)) by A38, FUNCT_1:59

.= F .: (F " {(F1 . i)}) by A10, A34, A11, A33, A15, A36 ;

then A39: u = v by FUNCT_1:75, ZFMISC_1:18;

F . m = F /. m by A38, PARTFUN1:def 6;

hence (L (#) F1) . i = G1 . (f . i) by A21, A11, A35, A38, A39, A37, VECTSP_6:def 5; :: thesis: verum