let E be set ; for A being Subset of (E ^omega) holds
( (A *) ? = A * & (A ?) * = A * )
let A be Subset of (E ^omega); ( (A *) ? = A * & (A ?) * = A * )
thus (A *) ? =
{(<%> E)} \/ (A *)
by Th76
.=
A *
by FLANG_1:48, ZFMISC_1:40
; (A ?) * = A *
thus (A ?) * =
({(<%> E)} \/ A) *
by Th76
.=
A *
by FLANG_1:48, FLANG_1:68
; verum