let E be set ; :: thesis: for A, B being Subset of (E ^omega)
for k being Nat st B c= A * holds
( (A |^.. k) ^^ B c= A |^.. k & B ^^ (A |^.. k) c= A |^.. k )
let A, B be Subset of (E ^omega); :: thesis: for k being Nat st B c= A * holds
( (A |^.. k) ^^ B c= A |^.. k & B ^^ (A |^.. k) c= A |^.. k )
let k be Nat; :: thesis: ( B c= A * implies ( (A |^.. k) ^^ B c= A |^.. k & B ^^ (A |^.. k) c= A |^.. k ) )
assume A1: B c= A * ; :: thesis: ( (A |^.. k) ^^ B c= A |^.. k & B ^^ (A |^.. k) c= A |^.. k )
then B ^^ (A |^.. k) c= (A *) ^^ (A |^.. k) by FLANG_1:17;
then A2: B ^^ (A |^.. k) c= (A |^.. k) ^^ (A *) by Th32;
(A |^.. k) ^^ B c= (A |^.. k) ^^ (A *) by A1, FLANG_1:17;
hence ( (A |^.. k) ^^ B c= A |^.. k & B ^^ (A |^.. k) c= A |^.. k ) by A2, Th17; :: thesis: verum