let X, Y, Z, V1, V2 be set ; :: thesis: for f being Function st ( curry f in Funcs (X,(Funcs (Y,Z))) or curry' f in Funcs (Y,(Funcs (X,Z))) ) & dom f c= [:V1,V2:] holds
f in Funcs ([:X,Y:],Z)
let f be Function; :: thesis: ( ( curry f in Funcs (X,(Funcs (Y,Z))) or curry' f in Funcs (Y,(Funcs (X,Z))) ) & dom f c= [:V1,V2:] implies f in Funcs ([:X,Y:],Z) )
assume ( curry f in Funcs (X,(Funcs (Y,Z))) or curry' f in Funcs (Y,(Funcs (X,Z))) ) ; :: thesis: ( not dom f c= [:V1,V2:] or f in Funcs ([:X,Y:],Z) )
then A1: ( uncurry (curry f) in Funcs ([:X,Y:],Z) or uncurry' (curry' f) in Funcs ([:X,Y:],Z) ) by Th11;
assume dom f c= [:V1,V2:] ; :: thesis: f in Funcs ([:X,Y:],Z)
hence f in Funcs ([:X,Y:],Z) by A1, FUNCT_5:50; :: thesis: verum