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 A2: m <= n ; :: thesis: A |^ (m,(n + 1)) = (A |^ (m,n)) \/ (A |^ (n + 1))

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

end;

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

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

end;

end;