let f be C -defined Function; :: thesis: ( f = seq *' implies f is total )
assume f = seq *' ; :: thesis: f is total
hence dom f = dom seq by Def1
.= C by PARTFUN1:def 2 ;
:: according to PARTFUN1:def 2 :: thesis: verum