let B be non empty set ; :: thesis: for A, X being set
for phi being Element of Funcs (A,B) holds phi | X = phi | (A /\ X)
let A, X be set ; :: thesis: for phi being Element of Funcs (A,B) holds phi | X = phi | (A /\ X)
let phi be Element of Funcs (A,B); :: thesis: phi | X = phi | (A /\ X)
dom phi = A by FUNCT_2:def 1;
then A1: dom (phi | X) = ((dom phi) /\ A) /\ X by RELAT_1:61
.= (dom phi) /\ (A /\ X) by XBOOLE_1:16 ;
for x being object st x in dom (phi | X) holds
(phi | X) . x = phi . x by FUNCT_1:47;
hence phi | X = phi | (A /\ X) by A1, FUNCT_1:46; :: thesis: verum