let F be Function; :: thesis: for X, x1, x2 being set st [x1,x2] in dom F holds
F .: (X --> x1),(X --> x2) = X --> (F . x1,x2)
let X be set ; :: thesis: for x1, x2 being set st [x1,x2] in dom F holds
F .: (X --> x1),(X --> x2) = X --> (F . x1,x2)
let x1, x2 be set ; :: thesis: ( [x1,x2] in dom F implies F .: (X --> x1),(X --> x2) = X --> (F . x1,x2) )
assume A1: [x1,x2] in dom F ; :: thesis: F .: (X --> x1),(X --> x2) = X --> (F . x1,x2)
set f = X --> x1;
set g = X --> x2;
thus F .: (X --> x1),(X --> x2) = F * (X --> [x1,x2]) by Th7
.= X --> (F . x1,x2) by A1, FUNCOP_1:23 ; :: thesis: verum