:: deftheorem defines ^^ MSAFREE5:def 9 :
for I being FinSequence-membered set
for p being FinSequence holds p ^^ I = { (p ^ q) where q is Element of I : q in I } ;