set a = the Element of D;
reconsider A = {({(<*> D)} --> the Element of D)} as non empty set ;
take A ; :: thesis: for x being Element of A holds x is non empty homogeneous quasi_total PartFunc of (D *),D
let x be Element of A; :: thesis: x is non empty homogeneous quasi_total PartFunc of (D *),D
x = (<*> D) .--> the Element of D by TARSKI:def 1;
hence x is non empty homogeneous quasi_total PartFunc of (D *),D by Th17; :: thesis: verum