let f, g be Function; :: thesis: ( g c= f implies g = f | (dom g) )
assume A1: g c= f ; :: thesis: g = f | (dom g)
then dom g c= dom f by RELAT_1:11;
hence dom g = dom (f | (dom g)) by RELAT_1:62; :: according to FUNCT_1:def 11 :: thesis: for b₁ being object holds
( not b₁ in proj1 g or g . b₁ = (f | (dom g)) . b₁ )
let x be object ; :: thesis: ( not x in proj1 g or g . x = (f | (dom g)) . x )
assume A2: x in dom g ; :: thesis: g . x = (f | (dom g)) . x
hence g . x = f . x by A1, Th2
.= (f | (dom g)) . x by A2, FUNCT_1:49 ;
:: thesis: verum