let IT1, IT2 be Function of (SmallestPartition X),X; :: thesis: ( ( for x being Element of SmallestPartition X holds IT1 . x = DeTrivial x ) & ( for x being Element of SmallestPartition X holds IT2 . x = DeTrivial x ) implies IT1 = IT2 )

assume that

A2: for x being Element of SmallestPartition X holds IT1 . x = DeTrivial x and

A3: for x being Element of SmallestPartition X holds IT2 . x = DeTrivial x ; :: thesis: IT1 = IT2

assume that

A2: for x being Element of SmallestPartition X holds IT1 . x = DeTrivial x and

A3: for x being Element of SmallestPartition X holds IT2 . x = DeTrivial x ; :: thesis: IT1 = IT2

now :: thesis: for x being Element of SmallestPartition X holds IT1 . x = IT2 . x

hence
IT1 = IT2
by FUNCT_2:63; :: thesis: verumlet x be Element of SmallestPartition X; :: thesis: IT1 . x = IT2 . x

thus IT1 . x = DeTrivial x by A2

.= IT2 . x by A3 ; :: thesis: verum

end;thus IT1 . x = DeTrivial x by A2

.= IT2 . x by A3 ; :: thesis: verum