let x be set ; :: thesis: for g, h, f being Function st x in dom g & h = f \/ g holds
h . x = g . x
let g, h, f 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 4;
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:8; :: thesis: verum