let E, x be set ; :: thesis: for A being Subset of (E ^omega)

for k being Nat holds

( <%x%> in A |^.. k iff ( <%x%> in A & ( <%> E in A or k <= 1 ) ) )

let A be Subset of (E ^omega); :: thesis: for k being Nat holds

( <%x%> in A |^.. k iff ( <%x%> in A & ( <%> E in A or k <= 1 ) ) )

let k be Nat; :: thesis: ( <%x%> in A |^.. k iff ( <%x%> in A & ( <%> E in A or k <= 1 ) ) )

thus ( <%x%> in A |^.. k implies ( <%x%> in A & ( <%> E in A or k <= 1 ) ) ) :: thesis: ( <%x%> in A & ( <%> E in A or k <= 1 ) implies <%x%> in A |^.. k )

A1: <%x%> in A and

A2: ( <%> E in A or k <= 1 ) ; :: thesis: <%x%> in A |^.. k

for k being Nat holds

( <%x%> in A |^.. k iff ( <%x%> in A & ( <%> E in A or k <= 1 ) ) )

let A be Subset of (E ^omega); :: thesis: for k being Nat holds

( <%x%> in A |^.. k iff ( <%x%> in A & ( <%> E in A or k <= 1 ) ) )

let k be Nat; :: thesis: ( <%x%> in A |^.. k iff ( <%x%> in A & ( <%> E in A or k <= 1 ) ) )

thus ( <%x%> in A |^.. k implies ( <%x%> in A & ( <%> E in A or k <= 1 ) ) ) :: thesis: ( <%x%> in A & ( <%> E in A or k <= 1 ) implies <%x%> in A |^.. k )

proof

assume that
assume
<%x%> in A |^.. k
; :: thesis: ( <%x%> in A & ( <%> E in A or k <= 1 ) )

then ex m being Nat st

( k <= m & <%x%> in A |^ m ) by Th2;

hence ( <%x%> in A & ( <%> E in A or k <= 1 ) ) by FLANG_2:9; :: thesis: verum

end;then ex m being Nat st

( k <= m & <%x%> in A |^ m ) by Th2;

hence ( <%x%> in A & ( <%> E in A or k <= 1 ) ) by FLANG_2:9; :: thesis: verum

A1: <%x%> in A and

A2: ( <%> E in A or k <= 1 ) ; :: thesis: <%x%> in A |^.. k