let E be set ; :: thesis: for A being Subset of (E ^omega )
for n being Nat holds A |^ n,(n + 1) = (A |^ n) \/ (A |^ (n + 1))
let A be Subset of (E ^omega ); :: thesis: for n being Nat holds A |^ n,(n + 1) = (A |^ n) \/ (A |^ (n + 1))
let n be Nat; :: thesis: A |^ n,(n + 1) = (A |^ n) \/ (A |^ (n + 1))
thus A |^ n,(n + 1) = (A |^ n,n) \/ (A |^ (n + 1)) by Th26, NAT_1:11
.= (A |^ n) \/ (A |^ (n + 1)) by Th22 ; :: thesis: verum