let E, x be set ; 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 ); for m being Nat st x in A |^ (m + 1) holds
( x in (A * ) ^^ A & x in A ^^ (A * ) )
let m be Nat; ( x in A |^ (m + 1) implies ( x in (A * ) ^^ A & x in A ^^ (A * ) ) )
assume
x in A |^ (m + 1)
; ( 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
and
A3:
( b in A & x = a ^ b )
by Def1;
a in A *
by A2, Th42;
hence
x in (A * ) ^^ A
by A3, Def1; x in A ^^ (A * )
x in A ^^ (A |^ m)
by A1, Th33;
then consider a, b being Element of E ^omega such that
A4:
a in A
and
A5:
b in A |^ m
and
A6:
x = a ^ b
by Def1;
b in A *
by A5, Th42;
hence
x in A ^^ (A * )
by A4, A6, Def1; verum