let x, E be set ; :: thesis: for A being Subset of (E ^omega )
for n being Nat st x in A & x <> <%> E holds
A |^.. n <> {(<%> E)}
let A be Subset of (E ^omega ); :: thesis: for n being Nat st x in A & x <> <%> E holds
A |^.. n <> {(<%> E)}
let n be Nat; :: thesis: ( x in A & x <> <%> E implies A |^.. n <> {(<%> E)} )
assume A1: ( x in A & x <> <%> E ) ; :: thesis: A |^.. n <> {(<%> E)}

per cases ( n = 0 or n > 0 ) ;

suppose A2: n = 0 ; :: thesis: A |^.. n <> {(<%> E)}

x in A |^ 1 by A1, FLANG_1:26;
then x in A |^.. n by A2, Th2;
hence A |^.. n <> {(<%> E)} by A1, TARSKI:def 1; :: thesis: verum

end;

suppose n > 0 ; :: thesis: A |^.. n <> {(<%> E)}

then A3: A |^ n <> {(<%> E)} by A1, FLANG_2:7;
A |^ n <> {} by A1, FLANG_1:28;
then consider y being set such that
A4: ( y in A |^ n & y <> <%> E ) by A3, ZFMISC_1:41;
y in A |^.. n by A4, Th2;
hence A |^.. n <> {(<%> E)} by A4, TARSKI:def 1; :: thesis: verum

end;

end;