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;

now :: thesis: for x being object st x in DISJOINT_PAIRS A holds
(singleton (DISJOINT_PAIRS A)) . x in the carrier of (NormForm A)

let x be object ; :: thesis: ( x in DISJOINT_PAIRS A implies (singleton (DISJOINT_PAIRS A)) . x in the carrier of (NormForm A) )
assume x in DISJOINT_PAIRS A ; :: thesis: (singleton (DISJOINT_PAIRS A)) . x in the carrier of (NormForm A)
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: verum

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: for a being Element of DISJOINT_PAIRS A holds f . a = {a}
thus for a being Element of DISJOINT_PAIRS A holds f . a = {a} by SETWISEO:54; :: thesis: verum