let E, x be set ; :: thesis: for a, b being Element of E ^omega holds
( a ^ b = <%x%> iff ( ( a = <%> E & b = <%x%> ) or ( b = <%> E & a = <%x%> ) ) )
let a, b be Element of E ^omega ; :: thesis: ( a ^ b = <%x%> iff ( ( a = <%> E & b = <%x%> ) or ( b = <%> E & a = <%x%> ) ) )
thus ( not a ^ b = <%x%> or ( a = <%> E & b = <%x%> ) or ( b = <%> E & a = <%x%> ) ) :: thesis: ( ( ( a = <%> E & b = <%x%> ) or ( b = <%> E & a = <%x%> ) ) implies a ^ b = <%x%> )
proof
assume A1: a ^ b = <%x%> ; :: thesis: ( ( a = <%> E & b = <%x%> ) or ( b = <%> E & a = <%x%> ) )
then len (a ^ b) = 1 by AFINSQ_1:34;
then (len a) + (len b) = 1 by AFINSQ_1:17;
then ( ( len a = 1 & b = <%> E ) or ( a = <%> E & len b = 1 ) ) by Th3;
hence ( ( a = <%> E & b = <%x%> ) or ( b = <%> E & a = <%x%> ) ) by A1; :: thesis: verum
end;
assume ( ( a = <%> E & b = <%x%> ) or ( b = <%> E & a = <%x%> ) ) ; :: thesis: a ^ b = <%x%>
hence a ^ b = <%x%> ; :: thesis: verum