let P be FinSequence-membered set ; :: thesis: ( ( for p, q being FinSequence st p in P & q in P holds
dom p = dom q ) implies P is antichain-like )
assume A1: for p, q being FinSequence st p in P & q in P holds
dom p = dom q ; :: thesis: P is antichain-like
for p, q being FinSequence st p in P & p ^ q in P holds
p = p ^ q

proof

let p, q be FinSequence; :: thesis: ( p in P & p ^ q in P implies p = p ^ q )
assume A2: ( p in P & p ^ q in P ) ; :: thesis: p = p ^ q
set r = p ^ q;
dom p = dom (p ^ q) by A1, A2;
then p = (p ^ q) | (dom (p ^ q)) by FINSEQ_1:21
.= p ^ q ;
hence p = p ^ q ; :: thesis: verum

end;

hence P is antichain-like by Th40; :: thesis: verum