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

for k being Nat holds

( A ? c= A |^.. k iff ( k = 0 or <%> E in A ) )

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

( A ? c= A |^.. k iff ( k = 0 or <%> E in A ) )

let k be Nat; :: thesis: ( A ? c= A |^.. k iff ( k = 0 or <%> E in A ) )

thus ( not A ? c= A |^.. k or k = 0 or <%> E in A ) :: thesis: ( ( k = 0 or <%> E in A ) implies A ? c= A |^.. k )

then A |^.. k = A * by Th11;

hence A ? c= A |^.. k by FLANG_2:86; :: thesis: verum

for k being Nat holds

( A ? c= A |^.. k iff ( k = 0 or <%> E in A ) )

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

( A ? c= A |^.. k iff ( k = 0 or <%> E in A ) )

let k be Nat; :: thesis: ( A ? c= A |^.. k iff ( k = 0 or <%> E in A ) )

thus ( not A ? c= A |^.. k or k = 0 or <%> E in A ) :: thesis: ( ( k = 0 or <%> E in A ) implies A ? c= A |^.. k )

proof

assume
( k = 0 or <%> E in A )
; :: thesis: A ? c= A |^.. k
A1:
<%> E in A ?
by FLANG_2:78;

assume A ? c= A |^.. k ; :: thesis: ( k = 0 or <%> E in A )

hence ( k = 0 or <%> E in A ) by A1, Th10; :: thesis: verum

end;assume A ? c= A |^.. k ; :: thesis: ( k = 0 or <%> E in A )

hence ( k = 0 or <%> E in A ) by A1, Th10; :: thesis: verum

then A |^.. k = A * by Th11;

hence A ? c= A |^.. k by FLANG_2:86; :: thesis: verum