per cases ( not t is empty or t is empty ) ;

suppose A1: not t is empty ; :: thesis: { f where f is Function of s,t : not f is one-to-one } is Subset of (Funcs s,t)

{ f where f is Function of s,t : not f is one-to-one } c= Funcs s,t

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { f where f is Function of s,t : not f is one-to-one } or x in Funcs s,t )
assume x in { f where f is Function of s,t : not f is one-to-one } ; :: thesis: x in Funcs s,t
then ex f being Function of s,t st
( x = f & not f is one-to-one ) ;
hence x in Funcs s,t by A1, FUNCT_2:11; :: thesis: verum

end;

hence { f where f is Function of s,t : not f is one-to-one } is Subset of (Funcs s,t) ; :: thesis: verum

end;

suppose A2: t is empty ; :: thesis: { f where f is Function of s,t : not f is one-to-one } is Subset of (Funcs s,t)

{ f where f is Function of s,t : not f is one-to-one } = {}

proof

assume { f where f is Function of s,t : not f is one-to-one } <> {} ; :: thesis: contradiction
then consider x being set such that
Z: x in { f where f is Function of s,t : not f is one-to-one } by XBOOLE_0:def 1;
ex f being Function of s,t st
( x = f & not f is one-to-one ) by Z;
hence contradiction by A2; :: thesis: verum

end;

hence { f where f is Function of s,t : not f is one-to-one } is Subset of (Funcs s,t) by XBOOLE_1:2; :: thesis: verum

end;

end;