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 A1: 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 A2: x in dom (id A) by RELAT_1:71;
thus f +~ x,y = ((id A) * f) +* ((x .--> y) * f) by A1, RELAT_1:79
.= ((id A) +* (x .--> y)) * f by Th11
.= ((id A) +* x,y) * f by A2, Def3 ; :: thesis: verum

end;

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

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

end;

end;