let x, y be set ; :: thesis: for F being FinSequence st F = <*x,y*> & x misses y holds
F is disjoint_valued
let F be FinSequence; :: thesis: ( F = <*x,y*> & x misses y implies F is disjoint_valued )
assume A1: ( F = <*x,y*> & x misses y ) ; :: thesis: F is disjoint_valued

now :: thesis: for i, j being object st i <> j holds
F . i misses F . j

let i, j be object ; :: thesis: ( i <> j implies F . b₁ misses F . b₂ )
assume A6: i <> j ; :: thesis: F . b₁ misses F . b₂

per cases ( not i in dom F or not j in dom F or ( i in dom F & j in dom F ) ) ;

suppose ( not i in dom F or not j in dom F ) ; :: thesis: F . b₁ misses F . b₂

then ( F . i = {} or F . j = {} ) by FUNCT_1:def 2;
hence F . i misses F . j ; :: thesis: verum

end;

suppose A7: ( i in dom F & j in dom F ) ; :: thesis: F . b₁ misses F . b₂

( len F = 2 & F . 1 = x & F . 2 = y ) by A1, FINSEQ_1:44;
then ( i in {1,2} & j in {1,2} ) by A7, FINSEQ_1:def 3, FINSEQ_1:2;
then ( ( i = 1 or i = 2 ) & ( j = 1 or j = 2 ) ) by TARSKI:def 2;
hence F . i misses F . j by A1, A6; :: thesis: verum

end;

end;

end;

hence F is disjoint_valued by PROB_2:def 2; :: thesis: verum