let E be set ; :: thesis: for A being Subset of (E ^omega) holds A |^ 1 = A
let A be Subset of (E ^omega); :: thesis: A |^ 1 = A
consider concat being sequence of (bool (E ^omega)) such that
A1: A |^ 1 = concat . 1 and
A2: ( concat . 0 = {(<%> E)} & ( for i being Nat holds concat . (i + 1) = (concat . i) ^^ A ) ) by Def2;
thus A |^ 1 = concat . (0 + 1) by A1
.= {(<%> E)} ^^ A by A2
.= A by Th13 ; :: thesis: verum