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 Th6
.= X --> (F . (x1,x2)) by A1, FUNCOP_1:17 ; :: thesis: verum