let X, Y, x be set ; :: thesis: ( x in Funcs X,Y iff ( x is Function & proj1 x = X & proj2 x c= Y ) )

hereby :: thesis: ( x is Function & proj1 x = X & proj2 x c= Y implies x in Funcs X,Y )

assume x in Funcs X,Y ; :: thesis: ( x is Function & proj1 x = X & proj2 x c= Y )
then ex f being Function st
( x = f & dom f = X & rng f c= Y ) by FUNCT_2:def 2;
hence ( x is Function & proj1 x = X & proj2 x c= Y ) ; :: thesis: verum

end;

assume x is Function ; :: thesis: ( not proj1 x = X or not proj2 x c= Y or x in Funcs X,Y )
then reconsider x = x as Function ;
dom x = proj1 x ;
hence ( not proj1 x = X or not proj2 x c= Y or x in Funcs X,Y ) by FUNCT_2:def 2; :: thesis: verum