let Omega be non empty finite set ; :: thesis: for f being PartFunc of Omega,REAL ex F being Finite_Sep_Sequence of Trivial-SigmaField Omega st
( dom f = union (rng F) & dom F = dom (canFS (dom f)) & ( for k being Nat st k in dom F holds
F . k = {((canFS (dom f)) . 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 PartFunc of Omega,REAL; :: thesis: ex F being Finite_Sep_Sequence of Trivial-SigmaField Omega st
( dom f = union (rng F) & dom F = dom (canFS (dom f)) & ( for k being Nat st k in dom F holds
F . k = {((canFS (dom f)) . 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 ) )
set Sigma = Trivial-SigmaField Omega;
set D = dom f;
defpred S₁[ Nat, set ] means $2 = {((canFS (dom f)) . $1)};
set L = len (canFS (dom f));
A1: for k being Nat st k in Seg (len (canFS (dom f))) holds
ex x being Element of bool Omega st S₁[k,x]

proof

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

end;

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

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
A4: ( i in dom F & j in dom F ) and
A5: i <> j ; :: thesis: F . i misses F . j
( i in dom (canFS (dom f)) & j in dom (canFS (dom f)) ) by A3, A4, FINSEQ_1:def 3;
then A6: (canFS (dom f)) . i <> (canFS (dom f)) . j by A5, FUNCT_1:def 4;
( F . i = {((canFS (dom f)) . i)} & F . j = {((canFS (dom f)) . j)} ) by A3, A4;
hence F . i misses F . j by A6, ZFMISC_1:11; :: thesis: verum

end;

then reconsider F = F as Finite_Sep_Sequence of Trivial-SigmaField Omega by MESFUNC3:4;

now :: thesis: for x being object st x in rng (canFS (dom f)) holds
x in union (rng F)

let x be object ; :: thesis: ( x in rng (canFS (dom f)) implies x in union (rng F) )
assume x in rng (canFS (dom f)) ; :: thesis: x in union (rng F)
then consider n being object such that
A7: n in dom (canFS (dom f)) and
A8: x = (canFS (dom f)) . n by FUNCT_1:def 3;
A9: n in Seg (len (canFS (dom f))) by A7, FINSEQ_1:def 3;
reconsider n = n as Element of NAT by A7;
n in dom F by A3, A7, FINSEQ_1:def 3;
then A10: F . n in rng F by FUNCT_1:def 3;
x in {((canFS (dom f)) . n)} by A8, TARSKI:def 1;
then x in F . n by A3, A9;
hence x in union (rng F) by A10, TARSKI:def 4; :: thesis: verum

end;

then A11: rng (canFS (dom f)) c= union (rng F) ;
take F ; :: thesis: ( dom f = union (rng F) & dom F = dom (canFS (dom f)) & ( for k being Nat st k in dom F holds
F . k = {((canFS (dom f)) . 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 ) )
A12: 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
A13: n in dom F and
A14: x in F . n and
A15: y in F . n ; :: thesis: f . x = f . y
A16: F . n = {((canFS (dom f)) . n)} by A3, A13;
hence f . x = f . ((canFS (dom f)) . n) by A14, TARSKI:def 1
.= f . y by A15, A16, TARSKI:def 1 ;
:: thesis: verum

end;

now :: thesis: for x being object st x in union (rng F) holds
x in rng (canFS (dom f))

let x be object ; :: thesis: ( x in union (rng F) implies x in rng (canFS (dom f)) )
assume x in union (rng F) ; :: thesis: x in rng (canFS (dom f))
then consider y being set such that
A17: x in y and
A18: y in rng F by TARSKI:def 4;
consider n being object such that
A19: n in dom F and
A20: y = F . n by A18, FUNCT_1:def 3;
reconsider n = n as Element of NAT by A19;
F . n = {((canFS (dom f)) . n)} by A3, A19;
then A21: x = (canFS (dom f)) . n by A17, A20, TARSKI:def 1;
n in dom (canFS (dom f)) by A3, A19, FINSEQ_1:def 3;
hence x in rng (canFS (dom f)) by A21, FUNCT_1:def 3; :: thesis: verum

end;

then union (rng F) c= rng (canFS (dom f)) ;
then union (rng F) = rng (canFS (dom f)) by A11;
hence ( dom f = union (rng F) & dom F = dom (canFS (dom f)) & ( for k being Nat st k in dom F holds
F . k = {((canFS (dom f)) . 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 A3, A12, FINSEQ_1:def 3, FUNCT_2:def 3; :: thesis: verum