let Omega be non empty finite set ; 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); 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; 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 ; 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; ( 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
; 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 S1[ Nat, set ] means $2 = f . (s . $1);
set Sigma = Trivial-SigmaField Omega;
set L = len s;
defpred S2[ 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 S2[k,x]
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
S2[k,F . k] ) )
from FINSEQ_1:sch 5(A3);
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
then A20:
dom f = union (rng F)
by A2, FUNCT_2:def 1;
take
F
; 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
A26:
for k being Nat st k in Seg (len s) holds
ex x being Element of REAL st S1[k,x]
ex a being FinSequence of REAL st
( dom a = Seg (len s) & ( for k being Nat st k in Seg (len s) holds
S1[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; verum