let A, B, a, b be set ; :: thesis: for f being Function of A,B st a in A & b in B holds

f +* (a .--> b) is Function of A,B

let f be Function of A,B; :: thesis: ( a in A & b in B implies f +* (a .--> b) is Function of A,B )

assume that

A1: a in A and

A2: b in B ; :: thesis: f +* (a .--> b) is Function of A,B

A3: {a} c= A by A1, ZFMISC_1:31;

set g = a .--> b;

set f1 = f +* (a .--> b);

rng (a .--> b) = {b} by FUNCOP_1:8;

then rng (a .--> b) c= B by A2, ZFMISC_1:31;

then A4: ( rng (f +* (a .--> b)) c= (rng f) \/ (rng (a .--> b)) & (rng f) \/ (rng (a .--> b)) c= B \/ B ) by FUNCT_4:17, XBOOLE_1:13;

dom (f +* (a .--> b)) = (dom f) \/ (dom (a .--> b)) by FUNCT_4:def 1

.= A \/ (dom (a .--> b)) by A2, FUNCT_2:def 1

.= A \/ {a}

.= A by A3, XBOOLE_1:12 ;

hence f +* (a .--> b) is Function of A,B by A4, FUNCT_2:2, XBOOLE_1:1; :: thesis: verum

f +* (a .--> b) is Function of A,B

let f be Function of A,B; :: thesis: ( a in A & b in B implies f +* (a .--> b) is Function of A,B )

assume that

A1: a in A and

A2: b in B ; :: thesis: f +* (a .--> b) is Function of A,B

A3: {a} c= A by A1, ZFMISC_1:31;

set g = a .--> b;

set f1 = f +* (a .--> b);

rng (a .--> b) = {b} by FUNCOP_1:8;

then rng (a .--> b) c= B by A2, ZFMISC_1:31;

then A4: ( rng (f +* (a .--> b)) c= (rng f) \/ (rng (a .--> b)) & (rng f) \/ (rng (a .--> b)) c= B \/ B ) by FUNCT_4:17, XBOOLE_1:13;

dom (f +* (a .--> b)) = (dom f) \/ (dom (a .--> b)) by FUNCT_4:def 1

.= A \/ (dom (a .--> b)) by A2, FUNCT_2:def 1

.= A \/ {a}

.= A by A3, XBOOLE_1:12 ;

hence f +* (a .--> b) is Function of A,B by A4, FUNCT_2:2, XBOOLE_1:1; :: thesis: verum