let E be set ; :: thesis: for A being Subset of (E ^omega)
for n being Nat holds
( <%> E in A |^.. n iff ( n = 0 or <%> E in A ) )
let A be Subset of (E ^omega); :: thesis: for n being Nat holds
( <%> E in A |^.. n iff ( n = 0 or <%> E in A ) )
let n be Nat; :: thesis: ( <%> E in A |^.. n iff ( n = 0 or <%> E in A ) )
thus ( not <%> E in A |^.. n or n = 0 or <%> E in A ) :: thesis: ( ( n = 0 or <%> E in A ) implies <%> E in A |^.. n )
proof
assume <%> E in A |^.. n ; :: thesis: ( n = 0 or <%> E in A )
then A1: ex k being Nat st
( n <= k & <%> E in A |^ k ) by Th2;
( n = 0 or n > 0 ) ;
hence ( n = 0 or <%> E in A ) by A1, FLANG_1:31; :: thesis: verum
end;
assume A2: ( n = 0 or <%> E in A ) ; :: thesis: <%> E in A |^.. n
per cases ( n = 0 or <%> E in A ) by A2;
suppose A3: n = 0 ; :: thesis: <%> E in A |^.. n
{(<%> E)} = A |^ 0 by FLANG_1:24;
then <%> E in A |^ n by A3, TARSKI:def 1;
hence <%> E in A |^.. n by Th2; :: thesis: verum
end;
suppose <%> E in A ; :: thesis: <%> E in A |^.. n
then <%> E in A |^ n by FLANG_1:30;
hence <%> E in A |^.. n by Th2; :: thesis: verum
end;
end;