:: deftheorem Def1 defines ^^ FLANG_1:def 1 :
for E being set
for A, B, b₄ being Subset of (E ^omega) holds
( b₄ = A ^^ B iff for x being set holds
( x in b₄ iff ex a, b being Element of E ^omega st
( a in A & b in B & x = a ^ b ) ) );