let IT, IT' be Function of A, Fin A; :: thesis: ( ( for x being set st x in A holds
IT . x = {x} ) & ( for x being set st x in A holds
IT' . x = {x} ) implies IT = IT' )
assume that
A3: for x being set st x in A holds
IT . x = {x} and
A4: for x being set st x in A holds
IT' . x = {x} ; :: thesis: IT = IT'

now

let x be set ; :: thesis: ( x in A implies IT . x = IT' . x )
assume x in A ; :: thesis: IT . x = IT' . x
then ( IT . x = {x} & IT' . x = {x} ) by A3, A4;
hence IT . x = IT' . x ; :: thesis: verum

end;

hence IT = IT' by FUNCT_2:18; :: thesis: verum