let E be set ; :: thesis: for A being Subset of (E ^omega)
for n being Nat holds (A |^ n) \/ (A |^.. (n + 1)) = A |^.. n
let A be Subset of (E ^omega); :: thesis: for n being Nat holds (A |^ n) \/ (A |^.. (n + 1)) = A |^.. n
let n be Nat; :: thesis: (A |^ n) \/ (A |^.. (n + 1)) = A |^.. n
A1: n <= n + 1 by NAT_1:13;
thus (A |^ n) \/ (A |^.. (n + 1)) = (A |^ (n,n)) \/ (A |^.. (n + 1)) by FLANG_2:22
.= A |^.. n by A1, Th7 ; :: thesis: verum