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 Th23;
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, Th41;
hence
x in (A *) ^^ A
by A3, Def1; x in A ^^ (A *)
x in A ^^ (A |^ m)
by A1, Th32;
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, Th41;
hence
x in A ^^ (A *)
by A4, A6, Def1; verum