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

now :: thesis: for x being object st x in A holds
IT . x = IT9 . x

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

end;

hence IT = IT9 by FUNCT_2:12; :: thesis: verum