let E be set ; :: thesis: for A being Subset of (E ^omega)
for k, l, n 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, l, n being Nat st <%> E in A & k <= n & l <= n holds
A |^ (k,n) = A |^ (l,n)
let k, l, n 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