let E, x 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 that
A1: x in A and
A2: x <> <%> E ; :: thesis: A |^.. n <> {(<%> E)}
per cases ( n = 0 or n > 0 ) ;
suppose A3: n = 0 ; :: thesis: A |^.. n <> {(<%> E)}
x in A |^ 1 by A1, FLANG_1:25;
then x in A |^.. n by A3, Th2;
hence A |^.. n <> {(<%> E)} by A2, TARSKI:def 1; :: thesis: verum
end;
suppose A4: n > 0 ; :: thesis: A |^.. n <> {(<%> E)}
A5: A |^ n <> {} by A1, FLANG_1:27;
A |^ n <> {(<%> E)} by A1, A2, A4, FLANG_2:7;
then consider y being object such that
A6: y in A |^ n and
A7: y <> <%> E by A5, ZFMISC_1:35;
y in A |^.. n by A6, Th2;
hence A |^.. n <> {(<%> E)} by A7, TARSKI:def 1; :: thesis: verum
end;
end;