:: deftheorem Def5 defines |^ PUA2MSS1:def 5 :
for A being partial non-empty UAStr
for R, b₃ being Relation of the carrier of A holds
( b₃ = R |^ A iff for x, y being Element of A holds
( [x,y] in b₃ iff ( [x,y] in R & ( for f being operation of A
for p, q being FinSequence st (p ^ <*x*>) ^ q in dom f & (p ^ <*y*>) ^ q in dom f holds
[(f . ((p ^ <*x*>) ^ q)),(f . ((p ^ <*y*>) ^ q))] in R ) ) ) );