:: deftheorem Def4 defines DomRel PUA2MSS1:def 4 :
for A being partial non-empty UAStr
for b₂ being Relation of the carrier of A holds
( b₂ = DomRel A iff for x, y being Element of A holds
( [x,y] in b₂ iff for f being operation of A
for p, q being FinSequence holds
( (p ^ <*x*>) ^ q in dom f iff (p ^ <*y*>) ^ q in dom f ) ) );