let E be set ; :: thesis:
let A be Subset of (E ^omega); :: thesis:

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

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

assume x in A ? ; :: thesis:
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:

end;

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

end;

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

end;