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 + 1) = (A |^ m,n) \/ (A |^ (n + 1))
let A be Subset of (E ^omega ); :: thesis: for m, n being Nat st m <= n + 1 holds
A |^ m,(n + 1) = (A |^ m,n) \/ (A |^ (n + 1))
let m, n be Nat; :: thesis: ( m <= n + 1 implies A |^ m,(n + 1) = (A |^ m,n) \/ (A |^ (n + 1)) )
assume A1: m <= n + 1 ; :: thesis: A |^ m,(n + 1) = (A |^ m,n) \/ (A |^ (n + 1))

per cases ( m <= n or m = n + 1 ) by A1, NAT_1:8;

suppose m <= n ; :: thesis: A |^ m,(n + 1) = (A |^ m,n) \/ (A |^ (n + 1))

then ( m <= n & n < n + 1 ) by NAT_1:13;
then A |^ m,(n + 1) = (A |^ m,n) \/ (A |^ (n + 1),(n + 1)) by Th25;
hence A |^ m,(n + 1) = (A |^ m,n) \/ (A |^ (n + 1)) by Th22; :: thesis: verum

end;

suppose A2: m = n + 1 ; :: thesis: A |^ m,(n + 1) = (A |^ m,n) \/ (A |^ (n + 1))

then A3: m > n by NAT_1:13;
thus A |^ m,(n + 1) = {} \/ (A |^ (n + 1)) by A2, Th22
.= (A |^ m,n) \/ (A |^ (n + 1)) by A3, Th21 ; :: thesis: verum

end;

end;