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

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