let E be set ; :: thesis: for A being Subset of (E ^omega )
for k, n, l being Nat st <%> E in A & k <= n & l <= n holds
A |^ k,n = A |^ l,n
let A be Subset of (E ^omega ); :: thesis: for k, n, l being Nat st <%> E in A & k <= n & l <= n holds
A |^ k,n = A |^ l,n
let k, n, l be Nat; :: thesis: ( <%> E in A & k <= n & l <= n implies A |^ k,n = A |^ l,n )
assume that
A1: <%> E in A and
A2: k <= n and
A3: l <= n ; :: thesis: A |^ k,n = A |^ l,n
thus A |^ k,n = A |^ n by A1, A2, Th34
.= A |^ l,n by A1, A3, Th34 ; :: thesis: verum