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 Th20;
assume dom f c= [:V1,V2:] ; :: thesis: f in Funcs [:X,Y:],Z
hence f in Funcs [:X,Y:],Z by A1, FUNCT_5:57; :: thesis: verum