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 object ; :: 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:8; :: 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 object such that
A3: 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 A3;
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;