let E be set ; :: thesis: for A being Subset of (E ^omega)
for m, n being Nat st <%> E in A & m <= n holds
A |^ (m,n) = A |^ n
let A be Subset of (E ^omega); :: thesis: for m, n being Nat st <%> E in A & m <= n holds
A |^ (m,n) = A |^ n
let m, n be Nat; :: thesis: ( <%> E in A & m <= n implies A |^ (m,n) = A |^ n )
assume that
A1: <%> E in A and
A2: m <= n ; :: thesis: A |^ (m,n) = A |^ n
A3: A |^ (m,n) c= A |^ n
proof
A4: now :: thesis: for k being Nat st k <= n holds
A |^ k c= A |^ n
let k be Nat; :: thesis: ( k <= n implies A |^ b1 c= A |^ n )
assume A5: k <= n ; :: thesis: A |^ b1 c= A |^ n
per cases ( k < n or k = n ) by A5, XXREAL_0:1;
suppose k < n ; :: thesis: A |^ b1 c= A |^ n
hence A |^ k c= A |^ n by A1, FLANG_1:36; :: thesis: verum
end;
suppose k = n ; :: thesis: A |^ b1 c= A |^ n
hence A |^ k c= A |^ n ; :: thesis: verum
end;
end;
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A |^ (m,n) or x in A |^ n )
assume x in A |^ (m,n) ; :: thesis: x in A |^ n
then consider k being Nat such that
m <= k and
A6: k <= n and
A7: x in A |^ k by Th19;
A |^ k c= A |^ n by A4, A6;
hence x in A |^ n by A7; :: thesis: verum
end;
A |^ n c= A |^ (m,n) by A2, Th20;
hence A |^ (m,n) = A |^ n by A3, XBOOLE_0:def 10; :: thesis: verum