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;