let g, f be Function; :: thesis: ( g c= f implies g = f | (dom g) )
assume Z: g c= f ; :: thesis: g = f | (dom g)
then dom g c= dom f by RELAT_1:25;
hence dom g = dom (f | (dom g)) by RELAT_1:91; :: according to FUNCT_1:def 17 :: thesis: for b₁ being set holds
( not b₁ in proj1 g or g . b₁ = (f | (dom g)) . b₁ )
let x be set ; :: thesis: ( not x in proj1 g or g . x = (f | (dom g)) . x )
assume Z1: x in dom g ; :: thesis: g . x = (f | (dom g)) . x
hence g . x = f . x by Z, Th8
.= (f | (dom g)) . x by Z1, FUNCT_1:72 ;
:: thesis: verum