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

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