let A, B be non empty set ; :: thesis: for f, g being Function of A,B
for x being Element of A st ( for y being Element of A st f . y <> g . y holds
y = x ) holds
f = g +* x,(f . x)
let f, g be Function of A,B; :: thesis: for x being Element of A st ( for y being Element of A st f . y <> g . y holds
y = x ) holds
f = g +* x,(f . x)
let x be Element of A; :: thesis: ( ( for y being Element of A st f . y <> g . y holds
y = x ) implies f = g +* x,(f . x) )
assume Z: for y being Element of A st f . y <> g . y holds
y = x ; :: thesis: f = g +* x,(f . x)
x in A ;
then A: x in dom g by FUNCT_2:def 1;
B: dom f = A by FUNCT_2:def 1
.= A \/ {x} by XBOOLE_1:12
.= (dom g) \/ {x} by FUNCT_2:def 1
.= (dom g) \/ (dom (x .--> (f . x))) by FUNCOP_1:19 ;
for e being set st e in (dom g) \/ (dom (x .--> (f . x))) holds
( ( e in dom (x .--> (f . x)) implies f . e = (x .--> (f . x)) . e ) & ( not e in dom (x .--> (f . x)) implies f . e = g . e ) )

proof

let e be set ; :: thesis: ( e in (dom g) \/ (dom (x .--> (f . x))) implies ( ( e in dom (x .--> (f . x)) implies f . e = (x .--> (f . x)) . e ) & ( not e in dom (x .--> (f . x)) implies f . e = g . e ) ) )
assume e in (dom g) \/ (dom (x .--> (f . x))) ; :: thesis: ( ( e in dom (x .--> (f . x)) implies f . e = (x .--> (f . x)) . e ) & ( not e in dom (x .--> (f . x)) implies f . e = g . e ) )
then X: e in A by B;
thus ( e in dom (x .--> (f . x)) implies f . e = (x .--> (f . x)) . e ) :: thesis: ( not e in dom (x .--> (f . x)) implies f . e = g . e )

proof

assume e in dom (x .--> (f . x)) ; :: thesis: f . e = (x .--> (f . x)) . e
then e in {x} by FUNCOP_1:19;
then e = x by TARSKI:def 1;
hence f . e = (x .--> (f . x)) . e by FUNCOP_1:87; :: thesis: verum

end;

assume not e in dom (x .--> (f . x)) ; :: thesis: f . e = g . e
then not e in {x} by FUNCOP_1:19;
then e <> x by TARSKI:def 1;
hence f . e = g . e by Z, X; :: thesis: verum

end;

hence f = g +* (x .--> (f . x)) by B, FUNCT_4:def 1
.= g +* x,(f . x) by A, Def3 ;
:: thesis: verum