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