let E be set ; :: thesis: for A being Subset of (E ^omega) holds A ? = (A |^ 0) \/ (A |^ 1)
let A be Subset of (E ^omega); :: thesis: A ? = (A |^ 0) \/ (A |^ 1)

now :: thesis: for x being object holds
( x in A ? iff ( x in A |^ 0 or x in A |^ 1 ) )

let x be object ; :: thesis: ( x in A ? iff ( x in A |^ 0 or x in A |^ 1 ) )
( x in A ? iff ex k being Nat st
( ( k = 0 or k = 1 ) & x in A |^ k ) )

proof

thus ( x in A ? implies ex k being Nat st
( ( k = 0 or k = 1 ) & x in A |^ k ) ) :: thesis: ( ex k being Nat st
( ( k = 0 or k = 1 ) & x in A |^ k ) implies x in A ? )

proof

assume x in A ? ; :: thesis: ex k being Nat st
( ( k = 0 or k = 1 ) & x in A |^ k )
then consider k being Nat such that
A1: k <= 1 and
A2: x in A |^ k by Th73;
( k = 0 or k = 1 ) by A1, NAT_1:25;
hence ex k being Nat st
( ( k = 0 or k = 1 ) & x in A |^ k ) by A2; :: thesis: verum

end;

given k being Nat such that A3: ( ( k = 0 or k = 1 ) & x in A |^ k ) ; :: thesis: x in A ?
thus x in A ? by A3, Th73; :: thesis: verum

end;

hence ( x in A ? iff ( x in A |^ 0 or x in A |^ 1 ) ) ; :: thesis: verum

end;

hence A ? = (A |^ 0) \/ (A |^ 1) by XBOOLE_0:def 3; :: thesis: verum