let A be set ; :: thesis: for f being Function
for x, y being set st rng f c= A holds
f +~ x,y = ((id A) +* x,y) * f
let f be Function; :: thesis: for x, y being set st rng f c= A holds
f +~ x,y = ((id A) +* x,y) * f
let x, y be set ; :: thesis: ( rng f c= A implies f +~ x,y = ((id A) +* x,y) * f )
assume Z: rng f c= A ; :: thesis: f +~ x,y = ((id A) +* x,y) * f

per cases ( x in A or not x in A ) ;

suppose x in A ; :: thesis: f +~ x,y = ((id A) +* x,y) * f

then S: x in dom (id A) by RELAT_1:71;
thus f +~ x,y = ((id A) * f) +* ((x .--> y) * f) by Z, RELAT_1:79
.= ((id A) +* (x .--> y)) * f by Th11
.= ((id A) +* x,y) * f by S, Def3 ; :: thesis: verum

end;

suppose S: not x in A ; :: thesis: f +~ x,y = ((id A) +* x,y) * f

then T: not x in dom (id A) ;
not x in rng f by S, Z;
hence f +~ x,y = f by FUNCT_4:109
.= (id A) * f by Z, RELAT_1:79
.= ((id A) +* x,y) * f by T, Def3 ;
:: thesis: verum

end;

end;