theorem Th52: :: HILB10_7:52

for F being FinSequence-yielding FinSequence
for g being FinSequence
for x being object holds doms (F ^ <*(g ^ <*x*>)*>) = (doms (F ^ <*g*>)) \/ { (f ^ <*(1 + (len g))*>) where f is Element of doms F : f in doms F }