let IT1, IT2 be Function of {_{X}_},X; :: thesis: ( ( for x being Element of {_{X}_} holds IT1 . x = DeTrivial x ) & ( for x being Element of {_{X}_} holds IT2 . x = DeTrivial x ) implies IT1 = IT2 )
assume that
B1: for x being Element of {_{X}_} holds IT1 . x = DeTrivial x and
B2: for x being Element of {_{X}_} holds IT2 . x = DeTrivial x ; :: thesis: IT1 = IT2

now

let x be Element of {_{X}_}; :: thesis: IT1 . x = IT2 . x
thus IT1 . x = DeTrivial x by B1
.= IT2 . x by B2 ; :: thesis: verum

end;

hence IT1 = IT2 by FUNCT_2:63; :: thesis: verum