let E be set ; :: thesis: for A, B being Subset of (E ^omega) holds
( <%> E in A ^^ B iff ( <%> E in A & <%> E in B ) )
let A, B be Subset of (E ^omega); :: thesis: ( <%> E in A ^^ B iff ( <%> E in A & <%> E in B ) )
thus ( <%> E in A ^^ B implies ( <%> E in A & <%> E in B ) ) :: thesis: ( <%> E in A & <%> E in B implies <%> E in A ^^ B )

proof

assume <%> E in A ^^ B ; :: thesis: ( <%> E in A & <%> E in B )
then ex a, b being Element of E ^omega st
( a in A & b in B & a ^ b = <%> E ) by Def1;
hence ( <%> E in A & <%> E in B ) by AFINSQ_1:30; :: thesis: verum

end;

assume ( <%> E in A & <%> E in B ) ; :: thesis: <%> E in A ^^ B
then {} ^ (<%> E) in A ^^ B by Def1;
hence <%> E in A ^^ B ; :: thesis: verum