let r1, r2 be Element of F_Real; :: thesis: ( ex F being FinSequence of (DivisibleMod L) st

( F is one-to-one & rng F = Carrier l & r1 = Sum (ScFS (v,l,F)) ) & ex F being FinSequence of (DivisibleMod 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 (DivisibleMod 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 (DivisibleMod 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 (DivisibleMod 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_{1}( 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_{1}(x) in dom F1

A10: for x being object st x in dom F1 holds

f . x = H_{1}(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

dom F1 c= rng f

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 defScFSDM;

A15: dom F1 = Seg (len F1) by FINSEQ_1:def 3

.= Seg (len G1) by defScFSDM

.= dom G1 by FINSEQ_1:def 3 ;

then reconsider f = f as Permutation of (dom G1) ;

A16: len G1 = len F2 by A7, defScFSDM

.= len (ScFS (v,l,F2)) by defScFSDM ;

for i being Nat st i in dom (ScFS (v,l,F2)) holds

(ScFS (v,l,F2)) . i = G1 . (f . i)

( F is one-to-one & rng F = Carrier l & r1 = Sum (ScFS (v,l,F)) ) & ex F being FinSequence of (DivisibleMod 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 (DivisibleMod 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 (DivisibleMod 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 (DivisibleMod 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

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

proof

consider f being Function of (dom F1),(dom F1) such that
let x be object ; :: thesis: ( x in dom F1 implies H_{1}(x) in dom F1 )

assume x in dom F1 ; :: thesis: H_{1}(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_{1}(x) in dom F1
by A1, FUNCT_1:33; :: thesis: verum

end;assume x in dom F1 ; :: thesis: H

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

A10: for x being object st x in dom F1 holds

f . x = H

for x1, x2 being object st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds

x1 = x2

proof

then A11:
f is one-to-one
;
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

F2 . x1 in rng F1 by A2, A5, A8, B1, 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;assume B1: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 ) ; :: thesis: x1 = x2

F2 . x1 in rng F1 by A2, A5, A8, B1, 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

dom F1 c= rng f

proof

then A12:
rng f = dom F1
;
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

F1 . y in rng F2 by A2, A5, B1, 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;assume B1: y in dom F1 ; :: thesis: y in rng f

F1 . y in rng F2 by A2, A5, B1, 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

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 defScFSDM;

A15: dom F1 = Seg (len F1) by FINSEQ_1:def 3

.= Seg (len G1) by defScFSDM

.= dom G1 by FINSEQ_1:def 3 ;

then reconsider f = f as Permutation of (dom G1) ;

A16: len G1 = len F2 by A7, defScFSDM

.= len (ScFS (v,l,F2)) by defScFSDM ;

for i being Nat st i in dom (ScFS (v,l,F2)) holds

(ScFS (v,l,F2)) . i = G1 . (f . i)

proof

hence
r1 = r2
by A3, A6, A16, RLVECT_2:6; :: thesis: verum
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 = (ScProductDM L) . (v,((l . (F2 /. i)) * (F2 /. i))) by B1, defScFSDM;

B3: i in dom F2 by A14, B1, FINSEQ_3:29;

then reconsider u = F2 . i as Element of (DivisibleMod 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 (DivisibleMod 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, defScFSDM, FUNCT_1:3; :: thesis: verum

end;assume B1: i in dom (ScFS (v,l,F2)) ; :: thesis: (ScFS (v,l,F2)) . i = G1 . (f . i)

B2: (ScFS (v,l,F2)) . i = (ScProductDM L) . (v,((l . (F2 /. i)) * (F2 /. i))) by B1, defScFSDM;

B3: i in dom F2 by A14, B1, FINSEQ_3:29;

then reconsider u = F2 . i as Element of (DivisibleMod 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 (DivisibleMod 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, defScFSDM, FUNCT_1:3; :: thesis: verum