A1: the carrier of (NormForm A) = Normal_forms_on A by NORMFORM:def 14;
set f = singleton (DISJOINT_PAIRS A);

A2: now

let x be set ; :: 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:67;
hence (singleton (DISJOINT_PAIRS A)) . x in the carrier of (NormForm A) by A1; :: thesis: verum

end;

dom (singleton (DISJOINT_PAIRS A)) = DISJOINT_PAIRS A by FUNCT_2:def 1;
then reconsider f = singleton (DISJOINT_PAIRS A) as Function of (DISJOINT_PAIRS A),the carrier of (NormForm A) by A2, FUNCT_2:5;
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:67; :: thesis: verum