let x be set ; :: thesis: for f, h, g being Function st x in dom f & h = f \/ g holds
h . x = f . x
let f, h, g be Function; :: thesis: ( x in dom f & h = f \/ g implies h . x = f . x )
assume x in dom f ; :: thesis: ( not h = f \/ g or h . x = f . x )
then [x,(f . x)] in f by FUNCT_1:def 4;
then ( h = f \/ g implies [x,(f . x)] in h ) by XBOOLE_0:def 3;
hence ( not h = f \/ g or h . x = f . x ) by FUNCT_1:8; :: thesis: verum