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

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

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

take
p
; :: thesis: p is disjoint_valued
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 = {} hence p . n misses p . m ; :: thesis: verum

end;assume n <> m ; :: thesis: p . n misses p . m

p . n = {} hence p . n misses p . m ; :: thesis: verum

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