set f = the total PartFunc of X,U;
take the total PartFunc of X,U ; :: thesis: ( the total PartFunc of X,U is U -valued & the total PartFunc of X,U is total )
thus ( the total PartFunc of X,U is U -valued & the total PartFunc of X,U is total ) ; :: thesis: verum