let X, Y be set ; :: thesis: for f being PartFunc of X,Y st dom f = X holds
f is Function of X,Y
let f be PartFunc of X,Y; :: thesis: ( dom f = X implies f is Function of X,Y )
rng f c= Y ;
hence ( dom f = X implies f is Function of X,Y ) by Th2; :: thesis: verum