let x, X be set ; :: thesis: for g, f being Function st g c= f & x in X & X /\ (dom f) c= dom g holds
f . x = g . x
let g, f be Function; :: thesis: ( g c= f & x in X & X /\ (dom f) c= dom g implies f . x = g . x )
assume that
Z1: g c= f and
Z2: x in X and
Z3: X /\ (dom f) c= dom g ; :: thesis: f . x = g . x

per cases ( x in dom g or not x in dom g ) ;

suppose x in dom g ; :: thesis: f . x = g . x

hence f . x = g . x by Z1, Th8; :: thesis: verum

end;

suppose S: not x in dom g ; :: thesis: f . x = g . x

then not x in X /\ (dom f) by Z3;
then not x in dom f by Z2, XBOOLE_0:def 4;
hence f . x = {} by FUNCT_1:def 2
.= g . x by S, FUNCT_1:def 2 ;
:: thesis: verum

end;

end;