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