let a be object ; :: thesis: for F being Function-yielding Function
for f being Function holds doms (F +* (a,f)) = (doms F) +* (a,(dom f))
let F be Function-yielding Function; :: thesis: for f being Function holds doms (F +* (a,f)) = (doms F) +* (a,(dom f))
let f be Function; :: thesis: doms (F +* (a,f)) = (doms F) +* (a,(dom f))
A1: ( dom (doms (F +* (a,f))) = dom (F +* (a,f)) & dom (F +* (a,f)) = dom F & dom F = dom (doms F) & dom (doms F) = dom ((doms F) +* (a,(dom f))) ) by FUNCT_6:def 2, FUNCT_7:30;
hence dom (doms (F +* (a,f))) = dom ((doms F) +* (a,(dom f))) ; :: according to FUNCT_1:def 11 :: thesis: for b₁ being object holds
( not b₁ in proj1 (doms (F +* (a,f))) or (doms (F +* (a,f))) . b₁ = ((doms F) +* (a,(dom f))) . b₁ )
let b be object ; :: thesis: ( not b in proj1 (doms (F +* (a,f))) or (doms (F +* (a,f))) . b = ((doms F) +* (a,(dom f))) . b )
assume A2: b in dom (doms (F +* (a,f))) ; :: thesis: (doms (F +* (a,f))) . b = ((doms F) +* (a,(dom f))) . b
then A3: (doms (F +* (a,f))) . b = dom ((F +* (a,f)) . b) by A1, FUNCT_6:def 2;

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

suppose A4: a = b ; :: thesis: (doms (F +* (a,f))) . b = ((doms F) +* (a,(dom f))) . b

hence (doms (F +* (a,f))) . b = dom f by A1, A2, A3, FUNCT_7:31
.= ((doms F) +* (a,(dom f))) . b by A1, A2, A4, FUNCT_7:31 ;
:: thesis: verum

end;

suppose A4: a <> b ; :: thesis: (doms (F +* (a,f))) . b = ((doms F) +* (a,(dom f))) . b

hence (doms (F +* (a,f))) . b = dom (F . b) by A3, FUNCT_7:32
.= (doms F) . b by A1, A2, FUNCT_6:def 2
.= ((doms F) +* (a,(dom f))) . b by A4, FUNCT_7:32 ;
:: thesis: verum

end;

end;