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 A5: x in A ; :: thesis: IT . x = IT' . x
then IT . x = {x} by A3;
hence IT . x = IT' . x by A4, A5; :: thesis: verum

end;

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