let K be Ring; 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; 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; 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; 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; ( 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
; Sum (L (#) F) = Sum (L (#) F1)
set v1 = Sum (L (#) F);
set v2 = Sum (L (#) F1);
defpred S1[ 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 & S1[x,y] )
proof
let x be
object ;
( x in dom F implies ex y being object st
( y in dom F & S1[x,y] ) )
assume
x in dom F
;
ex y being object st
( y in dom F & S1[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
;
( y in dom F & S1[x,y] )
y in F " {(F1 . x)}
by A14, TARSKI:def 1;
hence
y in dom F
by FUNCT_1:def 7;
S1[x,y]
thus
S1[
x,
y]
by A14;
verum
end;
consider f being Function of (dom F),(dom F) such that
A15:
for x being object st x in dom F holds
S1[x,f . x]
from FUNCT_2:sch 1(A13);
A16:
rng f = dom F
proof
thus
rng f c= dom F
;
XBOOLE_0:def 10 dom F c= rng f
let y be
object ;
TARSKI:def 3 ( not y in dom F or y in rng f )
assume A17:
y in dom F
;
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;
verum
end;
reconsider G1 = L (#) F as FinSequence of V ;
A21:
len G1 = len F
by VECTSP_6:def 5;
A22:
f is one-to-one
proof
let y1,
y2 be
object ;
FUNCT_1:def 4 ( 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
;
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;
verum
end;
set G2 = L (#) F1;
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 for i being Nat st i in dom (L (#) F1) holds
(L (#) F1) . i = G1 . (f . i)let i be
Nat;
( i in dom (L (#) F1) implies (L (#) F1) . i = G1 . (f . i) )assume A36:
i in dom (L (#) F1)
;
(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;
verum end;
hence
Sum (L (#) F) = Sum (L (#) F1)
by A4, A5, A7, A8, A21, A34, FINSEQ_1:48, RLVECT_2:6; verum