let y be object ; :: according to TARSKI:def 3,RELAT_1:def 19 :: thesis: ( not y in rng (f +* (a,x)) or y in X )
assume y in rng (f +* (a,x)) ; :: thesis: y in X
then consider z being object such that
A1: ( z in dom (f +* (a,x)) & y = (f +* (a,x)) . z ) by FUNCT_1:def 3;
A2: ( dom (f +* (a,x)) = dom f & ( z = a or z <> a ) ) by FUNCT_7:30;
then ( y = x or y = f . z ) by A1, FUNCT_7:31, FUNCT_7:32;
hence y in X by A1, A2, FUNCT_1:102; :: thesis: verum