let E be set ; :: thesis: for A being Subset of (E ^omega)
for n being Nat holds
( A |^ n = {(<%> E)} iff ( n = 0 or A = {(<%> E)} ) )
let A be Subset of (E ^omega); :: thesis: for n being Nat holds
( A |^ n = {(<%> E)} iff ( n = 0 or A = {(<%> E)} ) )
let n be Nat; :: thesis: ( A |^ n = {(<%> E)} iff ( n = 0 or A = {(<%> E)} ) )
thus ( not A |^ n = {(<%> E)} or n = 0 or A = {(<%> E)} ) :: thesis: ( ( n = 0 or A = {(<%> E)} ) implies A |^ n = {(<%> E)} )
proof
assume A1: A |^ n = {(<%> E)} ; :: thesis: ( n = 0 or A = {(<%> E)} )
now :: thesis: ( n > 0 implies A = {(<%> E)} )
assume n > 0 ; :: thesis: A = {(<%> E)}
then consider m being Nat such that
A2: m + 1 = n by NAT_1:6;
A |^ n = (A |^ m) ^^ A by A2, Th23;
hence A = {(<%> E)} by A1, Th14; :: thesis: verum
end;
hence ( n = 0 or A = {(<%> E)} ) ; :: thesis: verum
end;
assume ( n = 0 or A = {(<%> E)} ) ; :: thesis: A |^ n = {(<%> E)}
hence A |^ n = {(<%> E)} by Th24, Th28; :: thesis: verum