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 A1: for y being Element of A st f . y <> g . y holds
y = x ; :: thesis: f = g +* (x,(f . x))
x in A ;
then A2: x in dom g by FUNCT_2:def 1;
A3: 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))) ;
for e being object 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 object ; :: 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 A4: 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 ) )
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} ;
then e = x by TARSKI:def 1;
hence f . e = (x .--> (f . x)) . e by FUNCOP_1:72; :: thesis: verum

end;

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

end;

hence f = g +* (x .--> (f . x)) by A3, FUNCT_4:def 1
.= g +* (x,(f . x)) by A2, Def2 ;
:: thesis: verum