let a1, a2 be Function; :: thesis: ( dom a1 = dom f & ( for x being object st x in dom f holds
a1 . x = [:(f . x),{x}:] ) & dom a2 = dom f & ( for x being object st x in dom f holds
a2 . x = [:(f . x),{x}:] ) implies a1 = a2 )
assume that
A9: dom a1 = dom f and
A10: for x being object st x in dom f holds
a1 . x = [:(f . x),{x}:] and
A11: dom a2 = dom f and
A12: for x being object st x in dom f holds
a2 . x = [:(f . x),{x}:] ; :: thesis: a1 = a2

now :: thesis: for x being object st x in dom f holds
a1 . x = a2 . x

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

end;

hence a1 = a2 by A9, A11; :: thesis: verum