let a1, a2 be Function; :: thesis: ( dom a1 = dom f & ( for x being set st x in dom f holds
a1 . x = [:(f . x),{x}:] ) & dom a2 = dom f & ( for x being set st x in dom f holds
a2 . x = [:(f . x),{x}:] ) implies a1 = a2 )
assume that
A6: dom a1 = dom f and
A7: for x being set st x in dom f holds
a1 . x = [:(f . x),{x}:] and
A8: dom a2 = dom f and
A9: for x being set st x in dom f holds
a2 . x = [:(f . x),{x}:] ; :: thesis: a1 = a2

now

let x be set ; :: thesis: ( x in dom f implies a1 . x = a2 . x )
assume A10: x in dom f ; :: thesis: a1 . x = a2 . x
then a1 . x = [:(f . x),{x}:] by A7;
hence a1 . x = a2 . x by A9, A10; :: thesis: verum

end;

hence a1 = a2 by A6, A8, FUNCT_1:2; :: thesis: verum