now :: thesis: ( f +* (i,x) is ManySortedSet of I & ( for y being object st y in I holds
not (f +* (i,x)) . y is empty ) )

thus f +* (i,x) is ManySortedSet of I ; :: thesis: for y being object st y in I holds
not (f +* (i,x)) . y is empty
let y be object ; :: thesis: ( y in I implies not (f +* (i,x)) . y is empty )
assume A1: y in I ; :: thesis: not (f +* (i,x)) . y is empty
dom f = I by PARTFUN1:def 2;
then ( ( y <> i implies (f +* (i,x)) . y = f . y ) & ( y = i implies (f +* (i,x)) . y = x ) ) by A1, FUNCT_7:31, FUNCT_7:32;
hence not (f +* (i,x)) . y is empty by A1; :: thesis: verum

end;

hence f +* (i,x) is non-empty ; :: thesis: verum