let x be object ; :: according to PARTFUN1:def 4,AOFA_L00:def 1 :: thesis: ( not x in (dom X) /\ (dom (Y +* (X | J))) or X . x = (Y +* (X | J)) . x )
assume A1: x in (dom X) /\ (dom (Y +* (X | J))) ; :: thesis: X . x = (Y +* (X | J)) . x
then A2: ( x in dom X & x in dom (Y +* (X | J)) & dom (Y +* (X | J)) = (dom Y) \/ (dom (X | J)) ) by XBOOLE_0:def 4, FUNCT_4:def 1;
thus (Y +* (X | J)) . x = (X | J) . x by A2, RELAT_1:57, FUNCT_4:13
.= X . x by A1, FUNCT_1:49 ; :: thesis: verum