let E be set ; :: thesis: for A being Subset of (E ^omega)
for n being Nat st <%> E in A holds
( A * = (A *) ^^ (A |^ n) & A * = (A |^ n) ^^ (A *) )
let A be Subset of (E ^omega); :: thesis: for n being Nat st <%> E in A holds
( A * = (A *) ^^ (A |^ n) & A * = (A |^ n) ^^ (A *) )
let n be Nat; :: thesis: ( <%> E in A implies ( A * = (A *) ^^ (A |^ n) & A * = (A |^ n) ^^ (A *) ) )
defpred S1[ Nat] means ( A * = (A *) ^^ (A |^ $1) & A * = (A |^ $1) ^^ (A *) );
A1: (A |^ 0) ^^ (A *) = {(<%> E)} ^^ (A *) by Th24
.= A * by Th13 ;
assume A2: <%> E in A ; :: thesis: ( A * = (A *) ^^ (A |^ n) & A * = (A |^ n) ^^ (A *) )
A3: now :: thesis: for n being Nat st S1[n] holds
S1[n + 1]
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume A4: S1[n] ; :: thesis: S1[n + 1]
A5: (A *) ^^ (A |^ (n + 1)) = (A *) ^^ ((A |^ n) ^^ A) by Th23
.= (A *) ^^ A by A4, Th18
.= A * by A2, Th54 ;
(A |^ (n + 1)) ^^ (A *) = ((A |^ n) ^^ A) ^^ (A *) by Th23
.= (A ^^ (A |^ n)) ^^ (A *) by Th32
.= A ^^ (A *) by A4, Th18
.= A * by A2, Th54 ;
hence S1[n + 1] by A5; :: thesis: verum
end;
(A *) ^^ (A |^ 0) = (A *) ^^ {(<%> E)} by Th24
.= A * by Th13 ;
then A6: S1[ 0 ] by A1;
for n being Nat holds S1[n] from NAT_1:sch 2(A6, A3);
 hence ( A * = (A *) ^^ (A |^ n) & A * = (A |^ n) ^^ (A *) ) ; :: thesis: verum