{} 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

take f ; :: thesis: f is disjoint_valued

A1: for n being object holds f . n = {}

f . x misses f . y :: according to PROB_2:def 2 :: thesis: verum

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

then reconsider f = <*{}*> as FinSequence of F by Def1;
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;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

take f ; :: thesis: f is disjoint_valued

A1: for n being object holds f . n = {}

proof

thus
for x, y being object st x <> y holds
let n be object ; :: thesis: f . n = {}

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

hence
f . n = {}
by FUNCT_1:def 2; :: thesis: verumassume
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;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

f . x misses f . y :: according to PROB_2:def 2 :: thesis: verum