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

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