let E, x 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 ex m being Nat st
( k <= m & <%x%> in A |^ m ) by Th2;
hence ( <%x%> in A & ( <%> E in A or k <= 1 ) ) by FLANG_2:9; :: thesis: verum
end;
assume that
A1: <%x%> in A and
A2: ( <%> 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:25;
suppose ( <%> E in A & k > 1 ) ; :: thesis: <%x%> in A |^.. k
then <%x%> in A |^ k by A1, 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 A1, FLANG_1:72; :: thesis: verum
end;
suppose k = 1 ; :: thesis: <%x%> in A |^.. k
then <%x%> in A |^ k by A1, FLANG_1:25;
hence <%x%> in A |^.. k by Th2; :: thesis: verum
end;
end;