let E be set ; 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); 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; ( m <= n + 1 implies A |^ (m,(n + 1)) = (A |^ (m,n)) \/ (A |^ (n + 1)) )
assume A1:
m <= n + 1
; A |^ (m,(n + 1)) = (A |^ (m,n)) \/ (A |^ (n + 1))