let X be set ; :: thesis: for x being object
for f, g being Function st g c= f & x in X & X /\ (dom f) c= dom g holds
f . x = g . x
let x be object ; :: thesis: for f, g being Function st g c= f & x in X & X /\ (dom f) c= dom g holds
f . x = g . x
let f, g be Function; :: thesis: ( g c= f & x in X & X /\ (dom f) c= dom g implies f . x = g . x )
assume that
A1: g c= f and
A2: x in X and
A3: 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 A1, Th2; :: thesis: verum

end;

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

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

end;

end;