let r1, r2 be Element of F_Real; :: thesis: ( 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)) ; :: thesis: ( 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)) ; :: thesis: r1 = r2
deffunc H1( object ) -> set = (F1 ") . (F2 . \$1);
A7: len F1 = len F2 by ;
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
proof
let x be object ; :: thesis: ( x in dom F1 implies H1(x) in dom F1 )
assume x in dom F1 ; :: thesis: H1(x) in dom F1
then F2 . x in rng F1 by ;
then F2 . x in dom (F1 ") by ;
then (F1 ") . (F2 . x) in rng (F1 ") by FUNCT_1:3;
hence H1(x) in dom F1 by ; :: thesis: verum
end;
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 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 ; :: thesis: ( 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 ) ; :: thesis: x1 = x2
then F2 . x1 in rng F1 by ;
then B4: F2 . x1 in dom (F1 ") by ;
F2 . x2 in rng F1 by ;
then B7: F2 . x2 in dom (F1 ") by ;
(F1 ") . (F2 . x1) = f . x1 by
.= (F1 ") . (F2 . x2) by ;
then F2 . x1 = F2 . x2 by ;
hence x1 = x2 by A4, A8, B1; :: thesis: verum
end;
then A11: f is one-to-one ;
dom F1 c= rng f
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in dom F1 or y in rng f )
assume B1: y in dom F1 ; :: thesis: y in rng f
then F1 . y in rng F2 by ;
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 ;
x in dom f by ;
hence y in rng f by ; :: thesis: verum
end;
then A12: rng f = dom F1 ;
then reconsider f = f as Permutation of (dom F1) by ;
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
.= 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; :: thesis: ( 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)) ; :: thesis: (ScFS (v,l,F2)) . i = G1 . (f . i)
B2: (ScFS (v,l,F2)) . i = <;v,((l . (F2 /. i)) * (F2 /. i));> by ;
B3: i in dom F2 by ;
then reconsider u = F2 . i as Element of L by FINSEQ_2:11;
B4: i in dom f by ;
then f . i in dom F1 by ;
then reconsider m = f . i as Element of NAT ;
reconsider w = F1 . m as Element of L by ;
B5: F2 . i in rng F1 by ;
B6: F1 . (f . i) = F1 . ((F1 ") . (F2 . i)) by A8, A10, B3
.= F2 . i by ;
( F1 . m = F1 /. m & F2 . i = F2 /. i ) by ;
hence (ScFS (v,l,F2)) . i = G1 . (f . i) by ; :: thesis: verum
end;
hence r1 = r2 by ; :: thesis: verum