let X, Y be set ; :: thesis: for f being PartFunc of , st dom f = X holds
f is Function of X,Y
let f be PartFunc of ,; :: 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 Th4; :: thesis: verum