let x be object ; :: thesis: for f being Function st x in dom (curry f) holds
(curry f) . x is Function
let f be Function; :: thesis: ( x in dom (curry f) implies (curry f) . x is Function )
assume A1: x in dom (curry f) ; :: thesis: (curry f) . x is Function
dom (curry f) = proj1 (dom f) by Def1;
then ex g being Function st
( (curry f) . x = g & dom g = proj2 ((dom f) /\ [:{x},(proj2 (dom f)):]) & ( for y being object st y in dom g holds
g . y = f . (x,y) ) ) by A1, Def1;
hence (curry f) . x is Function ; :: thesis: verum