A1: for f being Function st f in dom (F | X) holds
(F | X) . f = uncurry f

proof

let f be Function; :: thesis: ( f in dom (F | X) implies (F | X) . f = uncurry f )
assume A2: f in dom (F | X) ; :: thesis: (F | X) . f = uncurry f
then A3: f in dom F by RELAT_1:57;
thus (F | X) . f = F . f by A2, FUNCT_1:47
.= uncurry f by A3, Def1 ; :: thesis: verum

end;

for x being set st x in dom (F | X) holds
x is Function-yielding Function

proof

let x be set ; :: thesis: ( x in dom (F | X) implies x is Function-yielding Function )
assume x in dom (F | X) ; :: thesis: x is Function-yielding Function
then x in dom F by RELAT_1:57;
hence x is Function-yielding Function by Def1; :: thesis: verum

end;

hence F | X is uncurrying by A1; :: thesis: verum