for B being non empty set
for A, X, Y being set st Funcs (X,Y) <> {} & X c= A & Y c= B holds
for f being Element of Funcs (X,Y) ex phi being Element of Funcs (A,B) st phi | X = f