let x, E be set ; :: thesis: for A being Subset of (E ^omega )
for m, n being Nat holds
( <%x%> in A |^ m,n iff ( <%x%> in A & m <= n & ( ( <%> E in A & n > 0 ) or ( m <= 1 & 1 <= n ) ) ) )
let A be Subset of (E ^omega ); :: thesis: for m, n being Nat holds
( <%x%> in A |^ m,n iff ( <%x%> in A & m <= n & ( ( <%> E in A & n > 0 ) or ( m <= 1 & 1 <= n ) ) ) )
let m, n be Nat; :: thesis: ( <%x%> in A |^ m,n iff ( <%x%> in A & m <= n & ( ( <%> E in A & n > 0 ) or ( m <= 1 & 1 <= n ) ) ) )
thus ( <%x%> in A |^ m,n implies ( <%x%> in A & m <= n & ( ( <%> E in A & n > 0 ) or ( m <= 1 & 1 <= n ) ) ) ) :: thesis: ( <%x%> in A & m <= n & ( ( <%> E in A & n > 0 ) or ( m <= 1 & 1 <= n ) ) implies <%x%> in A |^ m,n )

proof

assume A1: <%x%> in A |^ m,n ; :: thesis: ( <%x%> in A & m <= n & ( ( <%> E in A & n > 0 ) or ( m <= 1 & 1 <= n ) ) )
then consider mn being Nat such that
A2: ( m <= mn & mn <= n & <%x%> in A |^ mn ) by Th19;
thus ( <%x%> in A & m <= n & ( ( <%> E in A & n > 0 ) or ( m <= 1 & 1 <= n ) ) ) by A1, A2, Th9, Th21; :: thesis: verum

end;

assume A3: ( <%x%> in A & m <= n & ( ( <%> E in A & n > 0 ) or ( m <= 1 & 1 <= n ) ) ) ; :: thesis: <%x%> in A |^ m,n

per cases ( ( <%> E in A & n > 0 ) or ( m <= 1 & 1 <= n ) ) by A3;

suppose ( <%> E in A & n > 0 ) ; :: thesis: <%x%> in A |^ m,n

then A c= A |^ n by FLANG_1:36;
hence <%x%> in A |^ m,n by A3, Th19; :: thesis: verum

end;

suppose A4: ( m <= 1 & 1 <= n ) ; :: thesis: <%x%> in A |^ m,n

<%x%> in A |^ 1 by A3, FLANG_1:26;
hence <%x%> in A |^ m,n by A4, Th19; :: thesis: verum

end;

end;