thus ( ASeq is disjoint_valued implies for m, n being Nat st m <> n holds
ASeq . m misses ASeq . n ) ; :: thesis: ( ( for m, n being Nat st m <> n holds
ASeq . m misses ASeq . n ) implies ASeq is disjoint_valued )
A1: dom ASeq = NAT by FUNCT_2:def 1;
assume A2: for m, n being Nat st m <> n holds
ASeq . m misses ASeq . n ; :: thesis: ASeq is disjoint_valued
let x be object ; :: according to PROB_2:def 2 :: thesis: for y being object st x <> y holds
ASeq . x misses ASeq . y
let y be object ; :: thesis: ( x <> y implies ASeq . x misses ASeq . y )
assume A3: x <> y ; :: thesis: ASeq . x misses ASeq . y

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

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

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

end;

suppose ( not x in dom ASeq or not y in dom ASeq ) ; :: thesis: ASeq . x misses ASeq . y

then ( ASeq . x = {} or ASeq . y = {} ) by FUNCT_1:def 2;
hence ASeq . x misses ASeq . y by XBOOLE_1:65; :: thesis: verum

end;

end;