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

proof

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

end;

for x being set st x in dom (F | X) holds
( x is Function & proj1 x is Relation )

proof

let x be set ; :: thesis: ( x in dom (F | X) implies ( x is Function & proj1 x is Relation ) )
assume x in dom (F | X) ; :: thesis: ( x is Function & proj1 x is Relation )
then x in dom F by RELAT_1:57;
hence ( x is Function & proj1 x is Relation ) by Def2; :: thesis: verum

end;

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