set f = singleton (DISJOINT_PAIRS A);
A1: dom (singleton (DISJOINT_PAIRS A)) = DISJOINT_PAIRS A by FUNCT_2:def 1;
A2: the carrier of (NormForm A) = Normal_forms_on A by NORMFORM:def 12;

let x be object ; :: thesis:
assume x in DISJOINT_PAIRS A ; :: thesis:
then reconsider a = x as Element of DISJOINT_PAIRS A ;
(singleton (DISJOINT_PAIRS A)) . a = {a} by SETWISEO:54;
hence (singleton (DISJOINT_PAIRS A)) . x in the carrier of (NormForm A) by A2; :: thesis:

end;

then reconsider f = singleton (DISJOINT_PAIRS A) as Function of (DISJOINT_PAIRS A), the carrier of (NormForm A) by A1, FUNCT_2:3;
take f ; :: thesis:
thus for a being Element of DISJOINT_PAIRS A holds f . a = {a} by SETWISEO:54; :: thesis: