theorem Th64: :: POLNOT_1:64

for S being Polish-language
for p, q being Element of S
for r being Element of S ^^ 2 st r = p ^ q holds
decomp (S,2,r) = <*p,q*>