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 ) by FLANG_1:31; :: thesis: ( ( n = 0 or <%> E in A ) implies <%> E in A |^ n )
assume A1: ( n = 0 or <%> E in A ) ; :: thesis: <%> E in A |^ n

per cases ( n = 0 or <%> E in A ) by A1;

suppose n = 0 ; :: thesis: <%> E in A |^ n

then A |^ n = {(<%> E)} by FLANG_1:29;
hence <%> E in A |^ n by ZFMISC_1:31; :: thesis: verum

end;

suppose <%> E in A ; :: thesis: <%> E in A |^ n

hence <%> E in A |^ n by FLANG_1:30; :: thesis: verum

end;

end;