let E, x be set ; :: thesis: 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 ) ) )
let A, B be Subset of (E ^omega); :: thesis: ( <%x%> in A ^^ B iff ( ( <%> E in A & <%x%> in B ) or ( <%x%> in A & <%> E in B ) ) )
thus ( not <%x%> in A ^^ B or ( <%> E in A & <%x%> in B ) or ( <%x%> in A & <%> E in B ) ) :: thesis: ( ( ( <%> E in A & <%x%> in B ) or ( <%x%> in A & <%> E in B ) ) implies <%x%> in A ^^ B )

proof

assume <%x%> in A ^^ B ; :: thesis: ( ( <%> E in A & <%x%> in B ) or ( <%x%> in A & <%> E in B ) )
then ex a, b being Element of E ^omega st
( a in A & b in B & <%x%> = a ^ b ) by FLANG_1:def 1;
hence ( ( <%> E in A & <%x%> in B ) or ( <%x%> in A & <%> E in B ) ) by FLANG_1:4; :: thesis: verum

end;

A1: ( {} ^ <%x%> = <%x%> & <%x%> ^ {} = <%x%> ) ;
assume ( ( <%> E in A & <%x%> in B ) or ( <%x%> in A & <%> E in B ) ) ; :: thesis: <%x%> in A ^^ B
hence <%x%> in A ^^ B by A1, FLANG_1:def 1; :: thesis: verum