let E be set ; :: thesis: for A being Subset of (E ^omega )
for m, n being Nat st m <= n + 1 holds
(A |^ m,n) \/ (A |^.. (n + 1)) = A |^.. m
let A be Subset of (E ^omega ); :: thesis: for m, n being Nat st m <= n + 1 holds
(A |^ m,n) \/ (A |^.. (n + 1)) = A |^.. m
let m, n be Nat; :: thesis: ( m <= n + 1 implies (A |^ m,n) \/ (A |^.. (n + 1)) = A |^.. m )
assume m <= n + 1 ; :: thesis: (A |^ m,n) \/ (A |^.. (n + 1)) = A |^.. m
then A1: A |^.. (n + 1) c= A |^.. m by Th5;

now

let x be set ; :: thesis: ( x in A |^.. m implies x in (A |^ m,n) \/ (A |^.. (n + 1)) )
assume x in A |^.. m ; :: thesis: x in (A |^ m,n) \/ (A |^.. (n + 1))
then consider k being Nat such that
A2: m <= k and
A3: x in A |^ k by Th2;

A4: now

assume k > n ; :: thesis: x in A |^.. (n + 1)
then k >= n + 1 by NAT_1:13;
hence x in A |^.. (n + 1) by A3, Th2; :: thesis: verum

end;

( k <= n implies x in A |^ m,n ) by A2, A3, FLANG_2:19;
hence x in (A |^ m,n) \/ (A |^.. (n + 1)) by A4, XBOOLE_0:def 3; :: thesis: verum

end;

then A5: A |^.. m c= (A |^ m,n) \/ (A |^.. (n + 1)) by TARSKI:def 3;
A |^ m,n c= A |^.. m by Th6;
then (A |^ m,n) \/ (A |^.. (n + 1)) c= A |^.. m by A1, XBOOLE_1:8;
hence (A |^ m,n) \/ (A |^.. (n + 1)) = A |^.. m by A5, XBOOLE_0:def 10; :: thesis: verum