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