theorem :: FLANG_2:6

for E, x being set
for A, B being Subset of (E ^omega) holds
( <%x%> in A ^^ B iff ( ( <%> E in A & <%x%> in B ) or ( <%x%> in A & <%> E in B ) ) )