theorem Th54: :: HILB10_7:54

for F, G being FinSequence-yielding FinSequence holds (NAT -concatenation) .: [:(doms F),(doms G):] = doms (F ^ G)