reconsider A = {} as Element of S by PROB_1:4;
reconsider p = (Seg 1) --> A as Function of (Seg 1),S ;
A1: dom p = Seg 1 by FUNCOP_1:13;
then reconsider p = p as FinSequence by FINSEQ_1:def 2;
rng p c= S by RELAT_1:def 19;
then reconsider p = p as FinSequence of S by FINSEQ_1:def 4;
A2: for n, m being object st n <> m holds
p . n misses p . m

proof

let n, m be object ; :: thesis: ( n <> m implies p . n misses p . m )
assume n <> m ; :: thesis: p . n misses p . m
p . n = {}

proof

per cases ( n in dom p or not n in dom p ) ;

suppose n in dom p ; :: thesis: p . n = {}

hence p . n = {} by A1, FUNCOP_1:7; :: thesis: verum

end;

suppose not n in dom p ; :: thesis: p . n = {}

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

end;

end;

end;

hence p . n misses p . m ; :: thesis: verum

end;

take p ; :: thesis: p is disjoint_valued
thus p is disjoint_valued by A2, PROB_2:def 2; :: thesis: verum