let x be set ; :: 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 Def3;
then ex g being Function st
( (curry f) . x = g & dom g = proj2 ((dom f) /\ [:{x},(proj2 (dom f)):]) & ( for y being set st y in dom g holds
g . y = f . x,y ) ) by A1, Def3;
hence (curry f) . x is Function ; :: thesis: verum