let Omega be non empty finite set ; 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; 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 S1[ 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 S1[k,x]
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
S1[k,F . k] ) )
from FINSEQ_1:sch 5(A1);
then reconsider F = F as Finite_Sep_Sequence of Trivial-SigmaField Omega by MESFUNC3:4;
then A11:
rng (canFS (dom f)) c= union (rng F)
;
take
F
; ( 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
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; verum