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));
P1: 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 k in Seg (len (canFS (dom f))) ; :: thesis: ex x being Element of bool Omega st S₁[k,x]
then k in dom (canFS (dom f)) by FINSEQ_1:def 3;
then (canFS (dom f)) . k in rng (canFS (dom f)) by FUNCT_1:12;
then PPPP1: (canFS (dom f)) . k in dom f ;
take {((canFS (dom f)) . k)} ; :: thesis: ( {((canFS (dom f)) . k)} is Element of bool Omega & S₁[k,{((canFS (dom f)) . k)}] )
thus ( {((canFS (dom f)) . k)} is Element of bool Omega & S₁[k,{((canFS (dom f)) . k)}] ) by PPPP1, ZFMISC_1:37; :: thesis: verum

end;

consider F being FinSequence of bool Omega such that
P2: ( 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(P1);

now

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

end;

then reconsider F = F as Finite_Sep_Sequence of Trivial-SigmaField Omega by MESFUNC3:4;
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 ) )
PP3: union (rng F) = rng (canFS (dom f))

proof

now

let x be set ; :: 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
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;
reconsider n = n as Element of NAT by A3;
F . n = {((canFS (dom f)) . n)} by A3, P2;
then A5: x = (canFS (dom f)) . n by A2, A3, TARSKI:def 1;
n in dom (canFS (dom f)) by P2, A3, FINSEQ_1:def 3;
hence x in rng (canFS (dom f)) by FUNCT_1:def 5, A5; :: thesis: verum

end;

then A4: union (rng F) c= rng (canFS (dom f)) by TARSKI:def 3;

now

let x be set ; :: 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 set such that
A5: ( n in dom (canFS (dom f)) & x = (canFS (dom f)) . n ) by FUNCT_1:def 5;
A4: n in Seg (len (canFS (dom f))) 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 {((canFS (dom f)) . 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: verum

end;

then rng (canFS (dom f)) c= union (rng F) by TARSKI:def 3;
hence union (rng F) = rng (canFS (dom f)) by XBOOLE_0:def 10, A4; :: thesis: verum

end;

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 AS1: ( n in dom F & x in F . n & y in F . n ) ; :: thesis: f . x = f . y
P41: F . n = {((canFS (dom f)) . n)} by P2, AS1;
hence f . x = f . ((canFS (dom f)) . n) by AS1, TARSKI:def 1
.= f . y by P41, AS1, TARSKI:def 1 ;
:: thesis: verum

end;

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 FINSEQ_1:def 3, P2, PP3, FUNCT_2:def 3; :: thesis: verum