consider a being Element of D;
reconsider A = {({(<*> D)} --> a)} 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) .--> a by TARSKI:def 1;
hence x is non empty homogeneous quasi_total PartFunc of (D * ),D by Th54; :: thesis: verum