theorem Th7: :: FINSEQOP:7

for F being Function
for X, x1, x2 being set st [x1,x2] in dom F holds
F .: ((X --> x1),(X --> x2)) = X --> (F . (x1,x2))