let E be set ; :: thesis: for A being Subset of (E ^omega)
for m, n being Nat holds
( <%> E in A |^ (m,n) iff ( m = 0 or ( m <= n & <%> E in A ) ) )
let A be Subset of (E ^omega); :: thesis: for m, n being Nat holds
( <%> E in A |^ (m,n) iff ( m = 0 or ( m <= n & <%> E in A ) ) )
let m, n be Nat; :: thesis: ( <%> E in A |^ (m,n) iff ( m = 0 or ( m <= n & <%> E in A ) ) )
thus ( not <%> E in A |^ (m,n) or m = 0 or ( m <= n & <%> E in A ) ) :: thesis: ( ( m = 0 or ( m <= n & <%> E in A ) ) implies <%> E in A |^ (m,n) )
proof
assume that
A1: <%> E in A |^ (m,n) and
A2: ( m <> 0 & ( m > n or not <%> E in A ) ) ; :: thesis: contradiction
per cases ( ( m <> 0 & m > n ) or ( m <> 0 & not <%> E in A ) ) by A2;
suppose ( m <> 0 & m > n ) ; :: thesis: contradiction
hence contradiction by A1, Th21; :: thesis: verum
end;
suppose A3: ( m <> 0 & not <%> E in A ) ; :: thesis: contradiction
consider k being Nat such that
A4: m <= k and
k <= n and
A5: <%> E in A |^ k by A1, Th19;
k > 0 by A3, A4;
hence contradiction by A3, A5, FLANG_1:31; :: thesis: verum
end;
end;
end;
assume A6: ( m = 0 or ( m <= n & <%> E in A ) ) ; :: thesis: <%> E in A |^ (m,n)
per cases ( m = 0 or ( m <= n & <%> E in A ) ) by A6;
suppose A7: m = 0 ; :: thesis: <%> E in A |^ (m,n)
{(<%> E)} = A |^ 0 by FLANG_1:29;
then A8: {(<%> E)} c= A |^ (0,n) by Th20;
<%> E in {(<%> E)} by TARSKI:def 1;
hence <%> E in A |^ (m,n) by A7, A8; :: thesis: verum
end;
suppose ( m <= n & <%> E in A ) ; :: thesis: <%> E in A |^ (m,n)
then ( <%> E in A |^ m & A |^ m c= A |^ (m,n) ) by Th20, FLANG_1:30;
hence <%> E in A |^ (m,n) ; :: thesis: verum
end;
end;