let IT1, IT2 be Function of (DISJOINT_PAIRS A), the carrier of (NormForm A); :: thesis: ( ( for a being Element of DISJOINT_PAIRS A holds IT1 . a = {a} ) & ( for a being Element of DISJOINT_PAIRS A holds IT2 . a = {a} ) implies IT1 = IT2 )

assume that

A3: for a being Element of DISJOINT_PAIRS A holds IT1 . a = {a} and

A4: for a being Element of DISJOINT_PAIRS A holds IT2 . a = {a} ; :: thesis: IT1 = IT2

assume that

A3: for a being Element of DISJOINT_PAIRS A holds IT1 . a = {a} and

A4: for a being Element of DISJOINT_PAIRS A holds IT2 . a = {a} ; :: thesis: IT1 = IT2

now :: thesis: for a being Element of DISJOINT_PAIRS A holds IT1 . a = IT2 . a

hence
IT1 = IT2
by FUNCT_2:63; :: thesis: verumlet a be Element of DISJOINT_PAIRS A; :: thesis: IT1 . a = IT2 . a

IT1 . a = {a} by A3;

hence IT1 . a = IT2 . a by A4; :: thesis: verum

end;IT1 . a = {a} by A3;

hence IT1 . a = IT2 . a by A4; :: thesis: verum