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

proof

let x, y be object ; :: according to PROB_2:def 2 :: 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:13;
then A4: x = 1 by FINSEQ_1:2, TARSKI:def 1;
y in Seg 1 by A3, FUNCOP_1:13;
hence X . x misses X . y by A2, A4, FINSEQ_1:2, 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 2;
hence X . x misses X . y ; :: thesis: verum

end;

end;

end;

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