let v1, v2 be Element of V; ( ex F being FinSequence of the carrier of V st
( F is one-to-one & rng F = Carrier L & v1 = Sum (L (#) F) ) & ex F being FinSequence of the carrier of V st
( F is one-to-one & rng F = Carrier L & v2 = Sum (L (#) F) ) implies v1 = v2 )
given F1 being FinSequence of the carrier of V such that A3:
F1 is one-to-one
and
A4:
rng F1 = Carrier L
and
A5:
v1 = Sum (L (#) F1)
; ( for F being FinSequence of the carrier of V holds
( not F is one-to-one or not rng F = Carrier L or not v2 = Sum (L (#) F) ) or v1 = v2 )
given F2 being FinSequence of the carrier of V such that A6:
F2 is one-to-one
and
A7:
rng F2 = Carrier L
and
A8:
v2 = Sum (L (#) F2)
; v1 = v2
defpred S1[ object , object ] means {$2} = F1 " {(F2 . $1)};
A9:
len F1 = len F2
by A3, A4, A6, A7, FINSEQ_1:48;
A10:
dom F1 = Seg (len F1)
by FINSEQ_1:def 3;
A11:
dom F2 = Seg (len F2)
by FINSEQ_1:def 3;
A12:
for x being object st x in dom F1 holds
ex y being object st
( y in dom F1 & S1[x,y] )
proof
let x be
object ;
( x in dom F1 implies ex y being object st
( y in dom F1 & S1[x,y] ) )
assume
x in dom F1
;
ex y being object st
( y in dom F1 & S1[x,y] )
then
F2 . x in rng F1
by A4, A7, A9, A10, A11, FUNCT_1:def 3;
then consider y being
object such that A13:
F1 " {(F2 . x)} = {y}
by A3, FUNCT_1:74;
take
y
;
( y in dom F1 & S1[x,y] )
y in F1 " {(F2 . x)}
by A13, TARSKI:def 1;
hence
(
y in dom F1 &
S1[
x,
y] )
by A13, FUNCT_1:def 7;
verum
end;
consider f being Function of (dom F1),(dom F1) such that
A14:
for x being object st x in dom F1 holds
S1[x,f . x]
from FUNCT_2:sch 1(A12);
A15:
rng f = dom F1
proof
thus
rng f c= dom F1
by RELAT_1:def 19;
XBOOLE_0:def 10 dom F1 c= rng f
let y be
object ;
TARSKI:def 3 ( not y in dom F1 or y in rng f )
assume A16:
y in dom F1
;
y in rng f
then
F1 . y in rng F2
by A4, A7, FUNCT_1:def 3;
then consider x being
object such that A17:
x in dom F2
and A18:
F2 . x = F1 . y
by FUNCT_1:def 3;
F1 " {(F2 . x)} = F1 " (Im (F1,y))
by A16, A18, FUNCT_1:59;
then
F1 " {(F2 . x)} c= {y}
by A3, FUNCT_1:82;
then
{(f . x)} c= {y}
by A9, A10, A11, A14, A17;
then A19:
f . x = y
by ZFMISC_1:18;
x in dom f
by A9, A10, A11, A17, FUNCT_2:def 1;
hence
y in rng f
by A19, FUNCT_1:def 3;
verum
end;
set G1 = L (#) F1;
A20:
len (L (#) F1) = len F1
by Def5;
A21:
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 A22:
y1 in dom f
and A23:
y2 in dom f
and A24:
f . y1 = f . y2
;
y1 = y2
F2 . y1 in rng F1
by A4, A7, A9, A10, A11, A22, FUNCT_1:def 3;
then A25:
{(F2 . y1)} c= rng F1
by ZFMISC_1:31;
F2 . y2 in rng F1
by A4, A7, A9, A10, A11, A23, FUNCT_1:def 3;
then A26:
{(F2 . y2)} c= rng F1
by ZFMISC_1:31;
(
F1 " {(F2 . y1)} = {(f . y1)} &
F1 " {(F2 . y2)} = {(f . y2)} )
by A14, A22, A23;
then
{(F2 . y1)} = {(F2 . y2)}
by A24, A25, A26, FUNCT_1:91;
then
F2 . y1 = F2 . y2
by ZFMISC_1:3;
hence
y1 = y2
by A6, A9, A10, A11, A22, A23, FUNCT_1:def 4;
verum
end;
set G2 = L (#) F2;
A27:
dom (L (#) F2) = Seg (len (L (#) F2))
by FINSEQ_1:def 3;
reconsider f = f as Permutation of (dom F1) by A15, A21, FUNCT_2:57;
( dom F1 = Seg (len F1) & dom (L (#) F1) = Seg (len (L (#) F1)) )
by FINSEQ_1:def 3;
then reconsider f = f as Permutation of (dom (L (#) F1)) by A20;
A28:
len (L (#) F2) = len F2
by Def5;
A29:
dom (L (#) F1) = Seg (len (L (#) F1))
by FINSEQ_1:def 3;
now for i being Nat st i in dom (L (#) F2) holds
(L (#) F2) . i = (L (#) F1) . (f . i)let i be
Nat;
( i in dom (L (#) F2) implies (L (#) F2) . i = (L (#) F1) . (f . i) )assume A30:
i in dom (L (#) F2)
;
(L (#) F2) . i = (L (#) F1) . (f . i)then A31:
(
(L (#) F2) . i = (L . (F2 /. i)) * (F2 /. i) &
F2 . i = F2 /. i )
by A28, A11, A27, Def5, PARTFUN1:def 6;
i in dom f
by A9, A28, A10, A27, A30, FUNCT_2:def 1;
then A32:
f . i in dom F1
by A15, FUNCT_1:def 3;
then reconsider m =
f . i as
Element of
NAT ;
{(F1 . (f . i))} =
Im (
F1,
(f . i))
by A32, FUNCT_1:59
.=
F1 .: (F1 " {(F2 . i)})
by A9, A28, A10, A27, A14, A30
;
then A33:
F2 . i = F1 . m
by FUNCT_1:75, ZFMISC_1:18;
F1 . m = F1 /. m
by A32, PARTFUN1:def 6;
hence
(L (#) F2) . i = (L (#) F1) . (f . i)
by A20, A10, A29, A32, A33, A31, Def5;
verum end;
hence
v1 = v2
by A3, A4, A5, A6, A7, A8, A20, A28, FINSEQ_1:48, RLVECT_2:6; verum