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