let x, E be set ; :: thesis: for A being Subset of (E ^omega )
for k being Nat holds
( <%x%> in A |^.. k iff ( <%x%> in A & ( <%> E in A or k <= 1 ) ) )
let A be Subset of (E ^omega ); :: thesis: for k being Nat holds
( <%x%> in A |^.. k iff ( <%x%> in A & ( <%> E in A or k <= 1 ) ) )
let k be Nat; :: thesis: ( <%x%> in A |^.. k iff ( <%x%> in A & ( <%> E in A or k <= 1 ) ) )
thus ( <%x%> in A |^.. k implies ( <%x%> in A & ( <%> E in A or k <= 1 ) ) ) :: thesis: ( <%x%> in A & ( <%> E in A or k <= 1 ) implies <%x%> in A |^.. k )

proof

assume <%x%> in A |^.. k ; :: thesis: ( <%x%> in A & ( <%> E in A or k <= 1 ) )
then consider m being Nat such that
A1: ( k <= m & <%x%> in A |^ m ) by Th2;
thus ( <%x%> in A & ( <%> E in A or k <= 1 ) ) by A1, FLANG_2:9; :: thesis: verum

end;

assume A2: ( <%x%> in A & ( <%> E in A or k <= 1 ) ) ; :: thesis: <%x%> in A |^.. k

per cases ( ( <%> E in A & k > 1 ) or k = 0 or k = 1 ) by A2, NAT_1:26;

suppose ( <%> E in A & k > 1 ) ; :: thesis: <%x%> in A |^.. k

then <%x%> in A |^ k by A2, FLANG_2:9;
hence <%x%> in A |^.. k by Th2; :: thesis: verum

end;

suppose k = 0 ; :: thesis: <%x%> in A |^.. k

then A |^.. k = A * by Th11;
hence <%x%> in A |^.. k by A2, FLANG_1:73; :: thesis: verum

end;

suppose k = 1 ; :: thesis: <%x%> in A |^.. k

then <%x%> in A |^ k by A2, FLANG_1:26;
hence <%x%> in A |^.. k by Th2; :: thesis: verum

end;

end;