let E be set ; :: thesis: for B, A 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 B, A 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 B c= A * ; :: thesis: ( (A |^.. k) ^^ B c= A |^.. k & B ^^ (A |^.. k) c= A |^.. k )
then ( (A |^.. k) ^^ B c= (A |^.. k) ^^ (A * ) & B ^^ (A |^.. k) c= (A * ) ^^ (A |^.. k) ) by FLANG_1:18;
then ( (A |^.. k) ^^ B c= (A |^.. k) ^^ (A * ) & B ^^ (A |^.. k) c= (A |^.. k) ^^ (A * ) ) by Th32;
hence ( (A |^.. k) ^^ B c= A |^.. k & B ^^ (A |^.. k) c= A |^.. k ) by Th17; :: thesis: verum