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

proof

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

proof

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

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

thus p . n = {} by A1, A5, FUNCOP_1:13; :: thesis: verum

end;

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

thus p . n = {} by A6, FUNCT_1:def 4; :: thesis: verum

end;

end;

end;

thus p . n misses p . m by A4, XBOOLE_1:65; :: thesis: verum

end;

take p ; :: thesis: p is disjoint_valued
thus p is disjoint_valued by A3, PROB_2:def 3; :: thesis: verum