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

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