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 H₁( 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
H₁(x) in dom F1

proof

let x be object ; :: thesis: ( x in dom F1 implies H₁(x) in dom F1 )
assume x in dom F1 ; :: thesis: H₁(x) in dom F1
then F2 . x in rng F1 by A2, A5, A8, FUNCT_1:3;
then F2 . x in dom (F1 ") by A1, FUNCT_1:33;
then (F1 ") . (F2 . x) in rng (F1 ") by FUNCT_1:3;
hence H₁(x) in dom F1 by A1, FUNCT_1:33; :: 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 = H₁(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 ; :: 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 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; :: 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 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; :: thesis: 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; :: 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 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; :: thesis: verum

end;

hence r1 = r2 by A3, A6, A16, RLVECT_2:6; :: thesis: verum