let f be Element of A; :: thesis: f is ManySortedFunction of D,D
thus f is ManySortedFunction of D,D by Th19; :: thesis: verum