let b be object ; :: according to FUNCOP_1:def 6 :: thesis: ( not b in proj1 (F +* (a,f)) or (F +* (a,f)) . b is set )
assume b in dom (F +* (a,f)) ; :: thesis: (F +* (a,f)) . b is set
then A1: b in dom F by FUNCT_7:30;

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

suppose a = b ; :: thesis: (F +* (a,f)) . b is set

hence (F +* (a,f)) . b is set by A1, FUNCT_7:31; :: thesis: verum

end;

suppose a <> b ; :: thesis: (F +* (a,f)) . b is set

then (F +* (a,f)) . b = F . b by FUNCT_7:32;
hence (F +* (a,f)) . b is set ; :: thesis: verum

end;

end;