theorem Th14: :: PRALG_1:15

for p, q being 1-sorted-yielding FinSequence holds Carrier (p ^ q) = (Carrier p) ^ (Carrier q)