A3: dom f = I by PARTFUN1:def 2;
reconsider h = f +* (x,g) as ManySortedSet of I ;
h is ManySortedFunction of A,B

proof

let a be object ; :: according to PBOOLE:def 15 :: thesis: ( not a in I or h . a is Element of bool [:(A . a),(B . a):] )
assume a in I ; :: thesis: h . a is Element of bool [:(A . a),(B . a):]

per cases ( a = x or a <> x ) ;

suppose a = x ; :: thesis: h . a is Element of bool [:(A . a),(B . a):]

hence h . a is Function of (A . a),(B . a) by A3, FUNCT_7:31; :: thesis: verum

end;

suppose a <> x ; :: thesis: h . a is Element of bool [:(A . a),(B . a):]

then h . a = f . a by FUNCT_7:32;
hence h . a is Element of bool [:(A . a),(B . a):] ; :: thesis: verum

end;

end;

end;

hence f +* (x,g) is ManySortedFunction of A,B ; :: thesis: verum