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