consider a being Element of A;
reconsider X = 1 |-> a as FinSequence of A ;
A1: X is disjoint_valued

proof

let x, y be set ; :: according to PROB_2:def 3 :: thesis: ( x = y or X . x misses X . y )
assume A2: x <> y ; :: thesis: X . x misses X . y

per cases ( ( x in dom X & y in dom X ) or not x in dom X or not y in dom X ) ;

suppose A3: ( x in dom X & y in dom X ) ; :: thesis: X . x misses X . y

then x in Seg 1 by FUNCOP_1:19;
then A4: x = 1 by FINSEQ_1:4, TARSKI:def 1;
y in Seg 1 by A3, FUNCOP_1:19;
hence X . x misses X . y by A2, A4, FINSEQ_1:4, TARSKI:def 1; :: thesis: verum

end;

suppose ( not x in dom X or not y in dom X ) ; :: thesis: X . x misses X . y

then ( X . x = {} or X . y = {} ) by FUNCT_1:def 4;
hence X . x misses X . y by XBOOLE_1:65; :: thesis: verum

end;

end;

end;

not X is empty by FUNCOP_1:19, RELAT_1:60;
hence ex b₁ being FinSequence of A st
( not b₁ is empty & b₁ is disjoint_valued ) by A1; :: thesis: verum