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 ) :: thesis: ( ( n = 0 or <%> E in A ) implies <%> E in A |^.. n )

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 ) :: thesis: ( ( n = 0 or <%> E in A ) implies <%> E in A |^.. n )

proof

assume A2:
( n = 0 or <%> E in A )
; :: thesis: <%> E in A |^.. n
assume
<%> E in A |^.. n
; :: thesis: ( n = 0 or <%> E in A )

then A1: ex k being Nat st

( n <= k & <%> E in A |^ k ) by Th2;

( n = 0 or n > 0 ) ;

hence ( n = 0 or <%> E in A ) by A1, FLANG_1:31; :: thesis: verum

end;then A1: ex k being Nat st

( n <= k & <%> E in A |^ k ) by Th2;

( n = 0 or n > 0 ) ;

hence ( n = 0 or <%> E in A ) by A1, FLANG_1:31; :: thesis: verum