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