let E, x be set ; :: thesis: for A being Subset of (E ^omega )
for m being Nat st x in A |^ (m + 1) holds
( x in (A * ) ^^ A & x in A ^^ (A * ) )
let A be Subset of (E ^omega ); :: thesis: for m being Nat st x in A |^ (m + 1) holds
( x in (A * ) ^^ A & x in A ^^ (A * ) )
let m be Nat; :: thesis: ( x in A |^ (m + 1) implies ( x in (A * ) ^^ A & x in A ^^ (A * ) ) )
assume x in A |^ (m + 1) ; :: thesis: ( x in (A * ) ^^ A & x in A ^^ (A * ) )
then A1: x in (A |^ m) ^^ A by Th24;
then consider a, b being Element of E ^omega such that
A2: ( a in A |^ m & b in A & x = a ^ b ) by Def1;
( a in A * & b in A ) by A2, Th42;
hence x in (A * ) ^^ A by A2, Def1; :: thesis: x in A ^^ (A * )
x in A ^^ (A |^ m) by A1, Th33;
then consider a, b being Element of E ^omega such that
A3: ( a in A & b in A |^ m & x = a ^ b ) by Def1;
( a in A & b in A * ) by A3, Th42;
hence x in A ^^ (A * ) by A3, Def1; :: thesis: verum