let Omega be non empty finite set ; :: thesis:
let M be sigma_Measure of (Trivial-SigmaField Omega); :: thesis:
let f be Function of Omega,REAL ; :: thesis:
let x be FinSequence of ExtREAL ; :: thesis:
let s be FinSequence of Omega; :: thesis:
assume AS: ( M . Omega < +infty & s is one-to-one & rng s = Omega & len s = card Omega ) ; :: thesis:
set Sigma = Trivial-SigmaField Omega;
defpred S₁[ Nat, set ] means $2 = {(s . $1)};
set L = len s;
P1: for k being Nat st k in Seg (len s) holds
ex x being Element of bool Omega st S₁[k,x]

let k be Nat; :: thesis:
assume k in Seg (len s) ; :: thesis:
then k in dom s by FINSEQ_1:def 3;
then PP1PP: s . k in rng s by FUNCT_1:12;
take {(s . k)} ; :: thesis:
thus ( {(s . k)} is Element of bool Omega & S₁[k,{(s . k)}] ) by PP1PP, ZFMISC_1:37; :: thesis:

end;

consider F being FinSequence of bool Omega such that
P2: ( 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(P1);
defpred S₂[ Nat, set ] means $2 = f . (s . $1);
R1: for k being Nat st k in Seg (len s) holds
ex x being Element of REAL st S₂[k,x] ;
consider a being FinSequence of REAL such that
Q2: ( 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(R1);
Q1: dom F = dom s by P2, FINSEQ_1:def 3;

let i, j be Nat; :: thesis:
assume A1: ( i in dom F & j in dom F & i <> j ) ; :: thesis:
A4: ( i in dom s & j in dom s ) by FINSEQ_1:def 3, A1, P2;
PA3: s . i <> s . j by A1, A4, FUNCT_1:def 8, AS;
( F . i = {(s . i)} & F . j = {(s . j)} ) by A1, P2;
hence F . i misses F . j by ZFMISC_1:17, PA3; :: thesis:

end;

then reconsider F = F as Finite_Sep_Sequence of Trivial-SigmaField Omega by MESFUNC3:4;
take F ; :: thesis:
union (rng F) = rng s

let x be set ; :: thesis:
assume x in union (rng F) ; :: thesis:
then consider y being set such that
A2: ( x in y & y in rng F ) by TARSKI:def 4;
consider n being set such that
A3: ( n in dom F & y = F . n ) by A2, FUNCT_1:def 5;
F . n = {(s . n)} by A3, P2;
then A5: x = s . n by A2, A3, TARSKI:def 1;
n in dom s by P2, A3, FINSEQ_1:def 3;
hence x in rng s by FUNCT_1:def 5, A5; :: thesis:

end;

hence union (rng F) c= rng s by TARSKI:def 3; :: according to XBOOLE_0:def 10 :: thesis:
let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in rng s ; :: thesis:
then consider n being set such that
A5: ( n in dom s & x = s . n ) by FUNCT_1:def 5;
A4: n in Seg (len s) by A5, FINSEQ_1:def 3;
reconsider n = n as Element of NAT by A5;
A3: n in dom F by P2, A5, FINSEQ_1:def 3;
x in {(s . n)} by A5, TARSKI:def 1;
then A2: x in F . n by P2, A4;
F . n in rng F by A3, FUNCT_1:def 5;
hence x in union (rng F) by A2, TARSKI:def 4; :: thesis:

end;

then P3: dom f = union (rng F) by AS, FUNCT_2:def 1;
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 n be Nat; :: thesis:
let x, y be Element of Omega; :: thesis:
assume AS1: ( n in dom F & x in F . n & y in F . n ) ; :: thesis:
P41: F . n = {(s . n)} by P2, AS1;
thus f . x = f . (s . n) by P41, AS1, TARSKI:def 1
.= f . y by P41, AS1, TARSKI:def 1 ; :: thesis:

end;

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 Q1, P2, P3, Q2; :: thesis: