let E be set ; :: thesis: for A being Subset of (E ^omega) holds
( A ^^ {(<%> E)} = A & {(<%> E)} ^^ A = A )
let A be Subset of (E ^omega); :: thesis: ( A ^^ {(<%> E)} = A & {(<%> E)} ^^ A = A )
A1: for x being object st x in A ^^ {(<%> E)} holds
x in A
proof
let x be object ; :: thesis: ( x in A ^^ {(<%> E)} implies x in A )
assume x in A ^^ {(<%> E)} ; :: thesis: x in A
then consider a, d being Element of E ^omega such that
A2: a in A and
A3: ( d in {(<%> E)} & x = a ^ d ) by Def1;
x = a ^ {} by A3, TARSKI:def 1;
hence x in A by A2; :: thesis: verum
end;
A4: for x being object st x in A holds
x in {(<%> E)} ^^ A
proof
let x be object ; :: thesis: ( x in A implies x in {(<%> E)} ^^ A )
assume A5: x in A ; :: thesis: x in {(<%> E)} ^^ A
ex d, a being Element of E ^omega st
( d in {(<%> E)} & a in A & x = d ^ a )
proof
reconsider a = x as Element of E ^omega by A5;
consider d being Element of E ^omega such that
A6: d = <%> E ;
take d ; :: thesis: ex a being Element of E ^omega st
( d in {(<%> E)} & a in A & x = d ^ a )
take a ; :: thesis: ( d in {(<%> E)} & a in A & x = d ^ a )
thus ( d in {(<%> E)} & a in A & x = d ^ a ) by A5, A6, TARSKI:def 1; :: thesis: verum
end;
hence x in {(<%> E)} ^^ A by Def1; :: thesis: verum
end;
A7: for x being object st x in A holds
x in A ^^ {(<%> E)}
proof
let x be object ; :: thesis: ( x in A implies x in A ^^ {(<%> E)} )
assume A8: x in A ; :: thesis: x in A ^^ {(<%> E)}
ex a, d being Element of E ^omega st
( a in A & d in {(<%> E)} & x = a ^ d )
proof
reconsider a = x as Element of E ^omega by A8;
set d = <%> E;
take a ; :: thesis: ex d being Element of E ^omega st
( a in A & d in {(<%> E)} & x = a ^ d )
take <%> E ; :: thesis: ( a in A & <%> E in {(<%> E)} & x = a ^ (<%> E) )
thus ( a in A & <%> E in {(<%> E)} & x = a ^ (<%> E) ) by A8, TARSKI:def 1; :: thesis: verum
end;
hence x in A ^^ {(<%> E)} by Def1; :: thesis: verum
end;
for x being object st x in {(<%> E)} ^^ A holds
x in A
proof
let x be object ; :: thesis: ( x in {(<%> E)} ^^ A implies x in A )
assume x in {(<%> E)} ^^ A ; :: thesis: x in A
then consider d, a being Element of E ^omega such that
A9: d in {(<%> E)} and
A10: a in A and
A11: x = d ^ a by Def1;
x = {} ^ a by A9, A11, TARSKI:def 1;
hence x in A by A10; :: thesis: verum
end;
hence ( A ^^ {(<%> E)} = A & {(<%> E)} ^^ A = A ) by A1, A4, A7, TARSKI:2; :: thesis: verum