{} c= X ;
then reconsider f = <*{}*> as FinSequence of bool X by FINSEQ_1:74;
for k being Nat st k in dom f holds
f . k in F

proof

let k be Nat; :: thesis: ( k in dom f implies f . k in F )
assume k in dom f ; :: thesis: f . k in F
then k in Seg 1 by FINSEQ_1:def 8;
then k = 1 by FINSEQ_1:2, TARSKI:def 1;
then f . k = {} by FINSEQ_1:def 8;
hence f . k in F by PROB_1:4; :: thesis: verum

end;

then reconsider f = <*{}*> as FinSequence of F by Def1;
take f ; :: thesis: f is disjoint_valued
A1: for n being object holds f . n = {}

proof

let n be object ; :: thesis: f . n = {}

now :: thesis: ( n in dom f implies f . n = {} )

assume n in dom f ; :: thesis: f . n = {}
then n in Seg 1 by FINSEQ_1:def 8;
then n = 1 by FINSEQ_1:2, TARSKI:def 1;
hence f . n = {} by FINSEQ_1:def 8; :: thesis: verum

end;

hence f . n = {} by FUNCT_1:def 2; :: thesis: verum

end;

thus for x, y being object st x <> y holds
f . x misses f . y :: according to PROB_2:def 2 :: thesis: verum

proof

let x, y be object ; :: thesis: ( x <> y implies f . x misses f . y )
f . x = {} by A1;
hence ( x <> y implies f . x misses f . y ) by XBOOLE_1:65; :: thesis: verum

end;