let E, x be set ; :: thesis: for A being Subset of (E ^omega) st x in A & x <> <%> E holds

A + <> {(<%> E)}

let A be Subset of (E ^omega); :: thesis: ( x in A & x <> <%> E implies A + <> {(<%> E)} )

assume that

A1: x in A and

A2: x <> <%> E ; :: thesis: A + <> {(<%> E)}

A + = A |^.. 1 by Th50;

hence A + <> {(<%> E)} by A1, A2, Th14; :: thesis: verum

A + <> {(<%> E)}

let A be Subset of (E ^omega); :: thesis: ( x in A & x <> <%> E implies A + <> {(<%> E)} )

assume that

A1: x in A and

A2: x <> <%> E ; :: thesis: A + <> {(<%> E)}

A + = A |^.. 1 by Th50;

hence A + <> {(<%> E)} by A1, A2, Th14; :: thesis: verum