let v1, v2 be Element of V; :: thesis: ( 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 A4:
F1 is one-to-one
and
A5:
rng F1 = Carrier L
and
A6:
v1 = Sum (L (#) F1)
; :: thesis: ( 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 A7:
F2 is one-to-one
and
A8:
rng F2 = Carrier L
and
A9:
v2 = Sum (L (#) F2)
; :: thesis: v1 = v2
set G1 = L (#) F1;
set G2 = L (#) F2;
A10:
( len F1 = len F2 & len (L (#) F1) = len F1 & len (L (#) F2) = len F2 )
by A4, A5, A7, A8, Def8, FINSEQ_1:65;
A11:
( dom F1 = Seg (len F1) & dom F2 = Seg (len F2) )
by FINSEQ_1:def 3;
A12:
( dom (L (#) F1) = Seg (len (L (#) F1)) & dom (L (#) F2) = Seg (len (L (#) F2)) )
by FINSEQ_1:def 3;
defpred S1[ set , set ] means {$2} = F1 " {(F2 . $1)};
A13:
for x being set st x in dom F1 holds
ex y being set st
( y in dom F1 & S1[x,y] )
proof
let x be
set ;
:: thesis: ( x in dom F1 implies ex y being set st
( y in dom F1 & S1[x,y] ) )
assume
x in dom F1
;
:: thesis: ex y being set st
( y in dom F1 & S1[x,y] )
then
F2 . x in rng F1
by A5, A8, A10, A11, FUNCT_1:def 5;
then consider y being
set such that A14:
F1 " {(F2 . x)} = {y}
by A4, FUNCT_1:144;
take
y
;
:: thesis: ( y in dom F1 & S1[x,y] )
y in F1 " {(F2 . x)}
by A14, TARSKI:def 1;
hence
y in dom F1
by FUNCT_1:def 13;
:: thesis: S1[x,y]
thus
S1[
x,
y]
by A14;
:: thesis: verum
end;
A15:
( dom F1 = {} implies dom F1 = {} )
;
consider f being Function of (dom F1),(dom F1) such that
A16:
for x being set st x in dom F1 holds
S1[x,f . x]
from FUNCT_2:sch 1(A13);
A17:
rng f = dom F1
proof
thus
rng f c= dom F1
by RELAT_1:def 19;
:: according to XBOOLE_0:def 10 :: thesis: dom F1 c= rng f
let y be
set ;
:: according to TARSKI:def 3 :: thesis: ( not y in dom F1 or y in rng f )
assume A18:
y in dom F1
;
:: thesis: y in rng f
then
F1 . y in rng F2
by A5, A8, FUNCT_1:def 5;
then consider x being
set such that A19:
x in dom F2
and A20:
F2 . x = F1 . y
by FUNCT_1:def 5;
A21:
x in dom f
by A10, A11, A19, FUNCT_2:def 1;
F1 " {(F2 . x)} = F1 " (Im F1,y)
by A18, A20, FUNCT_1:117;
then
F1 " {(F2 . x)} c= {y}
by A4, FUNCT_1:152;
then
{(f . x)} c= {y}
by A10, A11, A16, A19;
then
f . x = y
by ZFMISC_1:24;
hence
y in rng f
by A21, FUNCT_1:def 5;
:: thesis: verum
end;
f is one-to-one
proof
let y1 be
set ;
:: according to FUNCT_1:def 8 :: thesis: for b1 being set holds
( not y1 in dom f or not b1 in dom f or not f . y1 = f . b1 or y1 = b1 )let y2 be
set ;
:: thesis: ( 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 &
y2 in dom f )
and A23:
f . y1 = f . y2
;
:: thesis: y1 = y2
A24:
(
y1 in dom F1 &
y2 in dom F1 )
by A15, A22, FUNCT_2:def 1;
then A25:
(
F1 " {(F2 . y1)} = {(f . y1)} &
F1 " {(F2 . y2)} = {(f . y2)} )
by A16;
(
F2 . y1 in rng F1 &
F2 . y2 in rng F1 )
by A5, A8, A10, A11, A24, FUNCT_1:def 5;
then
(
{(F2 . y1)} c= rng F1 &
{(F2 . y2)} c= rng F1 )
by ZFMISC_1:37;
then
{(F2 . y1)} = {(F2 . y2)}
by A23, A25, FUNCT_1:161;
then
(
F2 . y1 = F2 . y2 &
y1 in dom F2 &
y2 in dom F2 )
by A10, A11, A15, A22, FUNCT_2:def 1, ZFMISC_1:6;
hence
y1 = y2
by A7, FUNCT_1:def 8;
:: thesis: verum
end;
then reconsider f = f as Permutation of (dom F1) by A17, FUNCT_2:83;
( 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 A10;
now let i be
Element of
NAT ;
:: thesis: ( i in dom (L (#) F2) implies (L (#) F2) . i = (L (#) F1) . (f . i) )assume A26:
i in dom (L (#) F2)
;
:: thesis: (L (#) F2) . i = (L (#) F1) . (f . i)then
i in dom F2
by A10, FINSEQ_3:31;
then reconsider u =
F2 . i as
Element of
V by FINSEQ_2:13;
i in dom f
by A10, A12, A26, FUNCT_2:def 1;
then A27:
f . i in dom F1
by A17, FUNCT_1:def 5;
then reconsider m =
f . i as
Element of
NAT by A11;
reconsider v =
F1 . m as
Element of
V by A27, FINSEQ_2:13;
{(F1 . (f . i))} =
Im F1,
(f . i)
by A27, FUNCT_1:117
.=
F1 .: (F1 " {(F2 . i)})
by A10, A11, A12, A16, A26
;
then
{(F1 . (f . i))} c= {(F2 . i)}
by FUNCT_1:145;
then
(
u = v &
(L (#) F2) . i = (L . (F2 /. i)) * (F2 /. i) &
(L (#) F1) . m = (L . (F1 /. m)) * (F1 /. m) &
F1 . m = F1 /. m &
F2 . i = F2 /. i )
by A10, A11, A12, A26, A27, Def8, PARTFUN1:def 8, ZFMISC_1:24;
hence
(L (#) F2) . i = (L (#) F1) . (f . i)
;
:: thesis: verum end;
hence
v1 = v2
by A1, A6, A9, A10, RLVECT_2:8; :: thesis: verum