:: deftheorem defines ^ POLNOT_1:def 1 :
for D being non empty set
for P, Q being Subset of (D *) holds ^ (D,P,Q) = { (p ^ q) where p, q is FinSequence of D : ( p in P & q in Q ) } ;