let Omega be non empty finite set ; :: thesis: for M being sigma_Measure of (Trivial-SigmaField Omega)
for f being Function of Omega,REAL
for x being FinSequence of ExtREAL
for s being FinSequence of Omega st s is one-to-one & rng s = Omega holds
ex F being Finite_Sep_Sequence of Trivial-SigmaField Omega ex a being FinSequence of REAL st
( dom f = union (rng F) & dom a = dom s & dom F = dom s & ( for k being Nat st k in dom F holds
F . k = {(s . k)} ) & ( for n being Nat
for x, y being Element of Omega st n in dom F & x in F . n & y in F . n holds
f . x = f . y ) )
let M be sigma_Measure of (Trivial-SigmaField Omega); :: thesis: for f being Function of Omega,REAL
for x being FinSequence of ExtREAL
for s being FinSequence of Omega st s is one-to-one & rng s = Omega holds
ex F being Finite_Sep_Sequence of Trivial-SigmaField Omega ex a being FinSequence of REAL st
( dom f = union (rng F) & dom a = dom s & dom F = dom s & ( for k being Nat st k in dom F holds
F . k = {(s . k)} ) & ( for n being Nat
for x, y being Element of Omega st n in dom F & x in F . n & y in F . n holds
f . x = f . y ) )
let f be Function of Omega,REAL; :: thesis: for x being FinSequence of ExtREAL
for s being FinSequence of Omega st s is one-to-one & rng s = Omega holds
ex F being Finite_Sep_Sequence of Trivial-SigmaField Omega ex a being FinSequence of REAL st
( dom f = union (rng F) & dom a = dom s & dom F = dom s & ( for k being Nat st k in dom F holds
F . k = {(s . k)} ) & ( for n being Nat
for x, y being Element of Omega st n in dom F & x in F . n & y in F . n holds
f . x = f . y ) )
let x be FinSequence of ExtREAL ; :: thesis: for s being FinSequence of Omega st s is one-to-one & rng s = Omega holds
ex F being Finite_Sep_Sequence of Trivial-SigmaField Omega ex a being FinSequence of REAL st
( dom f = union (rng F) & dom a = dom s & dom F = dom s & ( for k being Nat st k in dom F holds
F . k = {(s . k)} ) & ( for n being Nat
for x, y being Element of Omega st n in dom F & x in F . n & y in F . n holds
f . x = f . y ) )
let s be FinSequence of Omega; :: thesis: ( s is one-to-one & rng s = Omega implies ex F being Finite_Sep_Sequence of Trivial-SigmaField Omega ex a being FinSequence of REAL st
( dom f = union (rng F) & dom a = dom s & dom F = dom s & ( for k being Nat st k in dom F holds
F . k = {(s . k)} ) & ( for n being Nat
for x, y being Element of Omega st n in dom F & x in F . n & y in F . n holds
f . x = f . y ) ) )
assume that
A1: s is one-to-one and
A2: rng s = Omega ; :: thesis: ex F being Finite_Sep_Sequence of Trivial-SigmaField Omega ex a being FinSequence of REAL st
( dom f = union (rng F) & dom a = dom s & dom F = dom s & ( for k being Nat st k in dom F holds
F . k = {(s . k)} ) & ( for n being Nat
for x, y being Element of Omega st n in dom F & x in F . n & y in F . n holds
f . x = f . y ) )
defpred S₁[ Nat, set ] means $2 = f . (s . $1);
set Sigma = Trivial-SigmaField Omega;
set L = len s;
defpred S₂[ Nat, set ] means $2 = {(s . $1)};
A3: for k being Nat st k in Seg (len s) holds
ex x being Element of bool Omega st S₂[k,x]

proof

let k be Nat; :: thesis: ( k in Seg (len s) implies ex x being Element of bool Omega st S₂[k,x] )
assume A4: k in Seg (len s) ; :: thesis: ex x being Element of bool Omega st S₂[k,x]
take {(s . k)} ; :: thesis: ( {(s . k)} is Element of bool Omega & S₂[k,{(s . k)}] )
k in dom s by A4, FINSEQ_1:def 3;
then s . k in rng s by FUNCT_1:3;
hence ( {(s . k)} is Element of bool Omega & S₂[k,{(s . k)}] ) by ZFMISC_1:31; :: thesis: verum

end;

consider F being FinSequence of bool Omega such that
A5: ( dom F = Seg (len s) & ( for k being Nat st k in Seg (len s) holds
S₂[k,F . k] ) ) from FINSEQ_1:sch 5(A3);

A6: now :: thesis: for i, j being Nat st i in dom F & j in dom F & i <> j holds
F . i misses F . j

let i, j be Nat; :: thesis: ( i in dom F & j in dom F & i <> j implies F . i misses F . j )
assume that
A7: ( i in dom F & j in dom F ) and
A8: i <> j ; :: thesis: F . i misses F . j
( i in dom s & j in dom s ) by A5, A7, FINSEQ_1:def 3;
then A9: s . i <> s . j by A1, A8, FUNCT_1:def 4;
( F . i = {(s . i)} & F . j = {(s . j)} ) by A5, A7;
hence F . i misses F . j by A9, ZFMISC_1:11; :: thesis: verum

end;

A10: dom F = dom s by A5, FINSEQ_1:def 3;
reconsider F = F as Finite_Sep_Sequence of Trivial-SigmaField Omega by A6, MESFUNC3:4;
union (rng F) = rng s

proof

now :: thesis: for x being object st x in union (rng F) holds
x in rng s

let x be object ; :: thesis: ( x in union (rng F) implies x in rng s )
assume x in union (rng F) ; :: thesis: x in rng s
then consider y being set such that
A11: x in y and
A12: y in rng F by TARSKI:def 4;
consider n being object such that
A13: n in dom F and
A14: y = F . n by A12, FUNCT_1:def 3;
F . n = {(s . n)} by A5, A13;
then A15: x = s . n by A11, A14, TARSKI:def 1;
n in dom s by A5, A13, FINSEQ_1:def 3;
hence x in rng s by A15, FUNCT_1:def 3; :: thesis: verum

end;

hence union (rng F) c= rng s ; :: according to XBOOLE_0:def 10 :: thesis: rng s c= union (rng F)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng s or x in union (rng F) )
assume x in rng s ; :: thesis: x in union (rng F)
then consider n being object such that
A16: n in dom s and
A17: x = s . n by FUNCT_1:def 3;
A18: n in Seg (len s) by A16, FINSEQ_1:def 3;
reconsider n = n as Element of NAT by A16;
n in dom F by A5, A16, FINSEQ_1:def 3;
then A19: F . n in rng F by FUNCT_1:def 3;
x in {(s . n)} by A17, TARSKI:def 1;
then x in F . n by A5, A18;
hence x in union (rng F) by A19, TARSKI:def 4; :: thesis: verum

end;

then A20: dom f = union (rng F) by A2, FUNCT_2:def 1;
take F ; :: thesis: ex a being FinSequence of REAL st
( dom f = union (rng F) & dom a = dom s & dom F = dom s & ( for k being Nat st k in dom F holds
F . k = {(s . k)} ) & ( for n being Nat
for x, y being Element of Omega st n in dom F & x in F . n & y in F . n holds
f . x = f . y ) )
A21: for n being Nat
for x, y being Element of Omega st n in dom F & x in F . n & y in F . n holds
f . x = f . y

proof

let n be Nat; :: thesis: for x, y being Element of Omega st n in dom F & x in F . n & y in F . n holds
f . x = f . y
let x, y be Element of Omega; :: thesis: ( n in dom F & x in F . n & y in F . n implies f . x = f . y )
assume that
A22: n in dom F and
A23: x in F . n and
A24: y in F . n ; :: thesis: f . x = f . y
A25: F . n = {(s . n)} by A5, A22;
hence f . x = f . (s . n) by A23, TARSKI:def 1
.= f . y by A24, A25, TARSKI:def 1 ;
:: thesis: verum

end;

A26: for k being Nat st k in Seg (len s) holds
ex x being Element of REAL st S₁[k,x]

proof

let k be Nat; :: thesis: ( k in Seg (len s) implies ex x being Element of REAL st S₁[k,x] )
f . (s . k) in REAL by XREAL_0:def 1;
hence ( k in Seg (len s) implies ex x being Element of REAL st S₁[k,x] ) ; :: thesis: verum

end;

ex a being FinSequence of REAL st
( dom a = Seg (len s) & ( for k being Nat st k in Seg (len s) holds
S₁[k,a . k] ) ) from FINSEQ_1:sch 5(A26);
hence ex a being FinSequence of REAL st
( dom f = union (rng F) & dom a = dom s & dom F = dom s & ( for k being Nat st k in dom F holds
F . k = {(s . k)} ) & ( for n being Nat
for x, y being Element of Omega st n in dom F & x in F . n & y in F . n holds
f . x = f . y ) ) by A5, A10, A20, A21; :: thesis: verum