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:20
.= ({(<%> E)} ^^ (A |^ k)) \/ ((A |^ k) ^^ A) by FLANG_1:32
.= (A |^ k) \/ ((A |^ k) ^^ A) by FLANG_1:13
.= ((A |^ k) ^^ {(<%> E)}) \/ ((A |^ k) ^^ A) by FLANG_1:13
.= (A |^ k) ^^ (A \/ {(<%> E)}) by FLANG_1:20
.= (A |^ k) ^^ (A ?) by Th76 ; :: thesis: verum