let E, x 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 ex mn being Nat st
( m <= mn & mn <= n & <%x%> in A |^ mn ) by Th19;
hence ( <%x%> in A & m <= n & ( ( <%> E in A & n > 0 ) or ( m <= 1 & 1 <= n ) ) ) by A1, Th9, Th21; :: thesis: verum
end;
assume that
A2: <%x%> in A and
A3: m <= n and
A4: ( ( <%> 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 A4;
suppose ( <%> E in A & n > 0 ) ; :: thesis: <%x%> in A |^ (m,n)
then A c= A |^ n by FLANG_1:35;
hence <%x%> in A |^ (m,n) by A2, A3, Th19; :: thesis: verum
end;
suppose A5: ( m <= 1 & 1 <= n ) ; :: thesis: <%x%> in A |^ (m,n)
<%x%> in A |^ 1 by A2, FLANG_1:25;
hence <%x%> in A |^ (m,n) by A5, Th19; :: thesis: verum
end;
end;