let r1, r2 be Element of F_Real; ( ex F being FinSequence of L st
( F is one-to-one & rng F = Carrier l & r1 = Sum (ScFS (v,l,F)) ) & ex F being FinSequence of L st
( F is one-to-one & rng F = Carrier l & r2 = Sum (ScFS (v,l,F)) ) implies r1 = r2 )
given F1 being FinSequence of L such that A1:
F1 is one-to-one
and
A2:
rng F1 = Carrier l
and
A3:
r1 = Sum (ScFS (v,l,F1))
; ( for F being FinSequence of L holds
( not F is one-to-one or not rng F = Carrier l or not r2 = Sum (ScFS (v,l,F)) ) or r1 = r2 )
given F2 being FinSequence of L such that A4:
F2 is one-to-one
and
A5:
rng F2 = Carrier l
and
A6:
r2 = Sum (ScFS (v,l,F2))
; r1 = r2
deffunc H1( object ) -> set = (F1 ") . (F2 . $1);
A7:
len F1 = len F2
by A1, A2, A4, A5, FINSEQ_1:48;
then A8:
dom F1 = dom F2
by FINSEQ_3:29;
A9:
for x being object st x in dom F1 holds
H1(x) in dom F1
consider f being Function of (dom F1),(dom F1) such that
A10:
for x being object st x in dom F1 holds
f . x = H1(x)
from FUNCT_2:sch 2(A9);
for x1, x2 being object st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds
x1 = x2
proof
let x1,
x2 be
object ;
( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 )
assume B1:
(
x1 in dom f &
x2 in dom f &
f . x1 = f . x2 )
;
x1 = x2
then
F2 . x1 in rng F1
by A2, A5, A8, FUNCT_1:3;
then B4:
F2 . x1 in dom (F1 ")
by A1, FUNCT_1:33;
F2 . x2 in rng F1
by A2, A5, A8, B1, FUNCT_1:3;
then B7:
F2 . x2 in dom (F1 ")
by A1, FUNCT_1:33;
(F1 ") . (F2 . x1) =
f . x1
by A10, B1
.=
(F1 ") . (F2 . x2)
by A10, B1
;
then
F2 . x1 = F2 . x2
by A1, B4, B7, FUNCT_1:def 4;
hence
x1 = x2
by A4, A8, B1;
verum
end;
then A11:
f is one-to-one
;
dom F1 c= rng f
proof
let y be
object ;
TARSKI:def 3 ( not y in dom F1 or y in rng f )
assume B1:
y in dom F1
;
y in rng f
then
F1 . y in rng F2
by A2, A5, FUNCT_1:3;
then consider x being
object such that B2:
(
x in dom F2 &
F2 . x = F1 . y )
by FUNCT_1:def 3;
B3:
f . x =
(F1 ") . (F2 . x)
by A8, A10, B2
.=
y
by A1, B1, B2, FUNCT_1:34
;
x in dom f
by A8, B2, FUNCT_2:def 1;
hence
y in rng f
by B3, FUNCT_1:3;
verum
end;
then A12:
rng f = dom F1
;
then reconsider f = f as Permutation of (dom F1) by A11, FUNCT_2:57;
reconsider G1 = ScFS (v,l,F1) as FinSequence of F_Real ;
set G2 = ScFS (v,l,F2);
A14:
len (ScFS (v,l,F2)) = len F2
by defScFS;
len F1 = len G1
by defScFS;
then A15:
dom F1 = dom G1
by FINSEQ_3:29;
then reconsider f = f as Permutation of (dom G1) ;
A16: len G1 =
len F2
by A7, defScFS
.=
len (ScFS (v,l,F2))
by defScFS
;
for i being Nat st i in dom (ScFS (v,l,F2)) holds
(ScFS (v,l,F2)) . i = G1 . (f . i)
proof
let i be
Nat;
( i in dom (ScFS (v,l,F2)) implies (ScFS (v,l,F2)) . i = G1 . (f . i) )
assume B1:
i in dom (ScFS (v,l,F2))
;
(ScFS (v,l,F2)) . i = G1 . (f . i)
B2:
(ScFS (v,l,F2)) . i = <;v,((l . (F2 /. i)) * (F2 /. i));>
by B1, defScFS;
B3:
i in dom F2
by A14, B1, FINSEQ_3:29;
then reconsider u =
F2 . i as
Element of
L by FINSEQ_2:11;
B4:
i in dom f
by A8, B3, FUNCT_2:def 1;
then
f . i in dom F1
by A12, FUNCT_1:3;
then reconsider m =
f . i as
Element of
NAT ;
reconsider w =
F1 . m as
Element of
L by A12, B4, FINSEQ_2:11, FUNCT_1:3;
B5:
F2 . i in rng F1
by A2, A5, B3, FUNCT_1:3;
B6:
F1 . (f . i) =
F1 . ((F1 ") . (F2 . i))
by A8, A10, B3
.=
F2 . i
by A1, B5, FUNCT_1:35
;
(
F1 . m = F1 /. m &
F2 . i = F2 /. i )
by A12, B3, B4, FUNCT_1:3, PARTFUN1:def 6;
hence
(ScFS (v,l,F2)) . i = G1 . (f . i)
by A12, A15, B2, B4, B6, defScFS, FUNCT_1:3;
verum
end;
hence
r1 = r2
by A3, A6, A16, RLVECT_2:6; verum