let g be Function; :: thesis: for x being set st dom g = {x} holds
g = x .--> (g . x)
let x be set ; :: thesis: ( dom g = {x} implies g = x .--> (g . x) )
assume A1: dom g = {x} ; :: thesis: g = x .--> (g . x)
now :: thesis: for a, b being object holds
( ( [a,b] in g implies [a,b] in x .--> (g . x) ) & ( [a,b] in x .--> (g . x) implies [a,b] in g ) )
let a, b be object ; :: thesis: ( ( [a,b] in g implies [a,b] in x .--> (g . x) ) & ( [a,b] in x .--> (g . x) implies [a,b] in g ) )
A2: dom (x .--> (g . x)) = {x} ;
hereby :: thesis: ( [a,b] in x .--> (g . x) implies [a,b] in g )
assume A3: [a,b] in g ; :: thesis: [a,b] in x .--> (g . x)
then A4: a in {x} by A1, FUNCT_1:1;
then A5: a = x by TARSKI:def 1;
then b = g . x by A3, FUNCT_1:1;
then (x .--> (g . x)) . a = b by A5, FUNCOP_1:72;
hence [a,b] in x .--> (g . x) by A2, A4, FUNCT_1:1; :: thesis: verum
end;
assume A6: [a,b] in x .--> (g . x) ; :: thesis: [a,b] in g
then A7: a in {x} by A2, FUNCT_1:1;
then A8: a = x by TARSKI:def 1;
b = (x .--> (g . x)) . a by A6, FUNCT_1:1
.= g . a by A8, FUNCOP_1:72 ;
hence [a,b] in g by A1, A7, FUNCT_1:1; :: thesis: verum
end;
hence g = x .--> (g . x) by RELAT_1:def 2; :: thesis: verum