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)}

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 )
;

end;

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;then x in A |^.. n by A3, Th2;

hence A |^.. n <> {(<%> E)} by A2, TARSKI:def 1; :: thesis: verum

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;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