thus dom (seq *' ) = dom seq by Def1
.= C by FUNCT_2:def 1 ; :: according to PARTFUN1:def 4 :: thesis: verum