let E be set ; :: thesis: for A being Subset of (E ^omega )
for k being Nat holds (A ? ) ^^ (A |^ k) = (A |^ k) ^^ (A ? )
let A be Subset of (E ^omega ); :: thesis: for k being Nat holds (A ? ) ^^ (A |^ k) = (A |^ k) ^^ (A ? )
let k be Nat; :: thesis: (A ? ) ^^ (A |^ k) = (A |^ k) ^^ (A ? )
thus (A ? ) ^^ (A |^ k) = ({(<%> E)} \/ A) ^^ (A |^ k) by Th76
.= ({(<%> E)} ^^ (A |^ k)) \/ (A ^^ (A |^ k)) by FLANG_1:21
.= ({(<%> E)} ^^ (A |^ k)) \/ ((A |^ k) ^^ A) by FLANG_1:33
.= (A |^ k) \/ ((A |^ k) ^^ A) by FLANG_1:14
.= ((A |^ k) ^^ {(<%> E)}) \/ ((A |^ k) ^^ A) by FLANG_1:14
.= (A |^ k) ^^ (A \/ {(<%> E)}) by FLANG_1:21
.= (A |^ k) ^^ (A ? ) by Th76 ; :: thesis: verum