let X be set ; :: thesis: for F being FinSequence of X holds
( F is disjoint_valued iff for i, j being Nat st i in dom F & j in dom F & i <> j holds
F . i misses F . j )
let F be FinSequence of X; :: thesis: ( F is disjoint_valued iff for i, j being Nat st i in dom F & j in dom F & i <> j holds
F . i misses F . j )

now :: thesis: ( ( for i, j being Nat st i in dom F & j in dom F & i <> j holds
F . i misses F . j ) implies F is disjoint_valued )

assume A1: for i, j being Nat st i in dom F & j in dom F & i <> j holds
F . i misses F . j ; :: thesis: F is disjoint_valued
for x, y being object st x <> y holds
F . x misses F . y

proof

let x, y be object ; :: thesis: ( x <> y implies F . x misses F . y )
assume A2: x <> y ; :: thesis: F . x misses F . y

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

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

hence F . x misses F . y by A1, A2; :: thesis: verum

end;

suppose not x in dom F ; :: thesis: F . x misses F . y

then F . x = {} by FUNCT_1:def 2;
hence F . x misses F . y ; :: thesis: verum

end;

suppose not y in dom F ; :: thesis: F . x misses F . y

then F . y = {} by FUNCT_1:def 2;
hence F . x misses F . y ; :: thesis: verum

end;

end;

end;

hence F is disjoint_valued by PROB_2:def 2; :: thesis: verum

end;

hence ( F is disjoint_valued iff for i, j being Nat st i in dom F & j in dom F & i <> j holds
F . i misses F . j ) by PROB_2:def 2; :: thesis: verum