theorem Th30: :: YELLOW18:30

for X, Y, x being set holds
( x in Funcs (X,Y) iff ( x is Function & proj1 x = X & proj2 x c= Y ) )