let E be set ; :: thesis: for A being Subset of () holds (A *) ^^ A = A |^.. 1
let A be Subset of (); :: thesis: (A *) ^^ A = A |^.. 1
A1: now :: thesis: for x being object st x in (A *) ^^ A holds
x in A |^.. 1
let x be object ; :: thesis: ( x in (A *) ^^ A implies x in A |^.. 1 )
assume x in (A *) ^^ A ; :: thesis: x in A |^.. 1
then consider a1, a2 being Element of E ^omega such that
A2: a1 in A * and
A3: a2 in A and
A4: x = a1 ^ a2 by FLANG_1:def 1;
consider n being Nat such that
A5: a1 in A |^ n by ;
A6: n + 1 >= 1 by NAT_1:11;
a2 in A |^ 1 by ;
then a1 ^ a2 in A |^ (n + 1) by ;
hence x in A |^.. 1 by A4, A6, Th2; :: thesis: verum
end;
now :: thesis: for x being object st x in A |^.. 1 holds
x in (A *) ^^ A
let x be object ; :: thesis: ( x in A |^.. 1 implies x in (A *) ^^ A )
assume x in A |^.. 1 ; :: thesis: x in (A *) ^^ A
then consider n being Nat such that
A7: n >= 1 and
A8: x in A |^ n by Th2;
consider m being Nat such that
A9: m + 1 = n by ;
A |^ (m + 1) c= (A *) ^^ A by FLANG_1:51;
hence x in (A *) ^^ A by A8, A9; :: thesis: verum
end;
hence (A *) ^^ A = A |^.. 1 by ; :: thesis: verum