let A be set ; :: thesis: for f being Function
for x, y being object st rng f c= A holds
f +~ (x,y) = ((id A) +* (x,y)) * f
let f be Function; :: thesis: for x, y being object st rng f c= A holds
f +~ (x,y) = ((id A) +* (x,y)) * f
let x, y be object ; :: 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) ;
thus f +~ (x,y) = ((id A) * f) +* ((x .--> y) * f) by A1, RELAT_1:53
.= ((id A) +* (x .--> y)) * f by Th10
.= ((id A) +* (x,y)) * f by A2, Def2 ; :: 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:103
.= (id A) * f by A1, RELAT_1:53
.= ((id A) +* (x,y)) * f by A4, Def2 ;
:: thesis: verum

end;

end;