set X = { F where F is Function of (REAL-NS (k . 1)),(REAL-NS (k . (n + 1))) : ex N being FinSequence st
( N is_Multilayer_perceptron_with k,n & F = OutPutFunc (N,k,n) ) } ;
set Y = Funcs ( the carrier of (REAL-NS (k . 1)), the carrier of (REAL-NS (k . (n + 1))));

now :: thesis: for z being object st z in { F where F is Function of (REAL-NS (k . 1)),(REAL-NS (k . (n + 1))) : ex N being FinSequence st
( N is_Multilayer_perceptron_with k,n & F = OutPutFunc (N,k,n) ) } holds
z in Funcs ( the carrier of (REAL-NS (k . 1)), the carrier of (REAL-NS (k . (n + 1))))

let z be object ; :: thesis: ( z in { F where F is Function of (REAL-NS (k . 1)),(REAL-NS (k . (n + 1))) : ex N being FinSequence st
( N is_Multilayer_perceptron_with k,n & F = OutPutFunc (N,k,n) ) } implies z in Funcs ( the carrier of (REAL-NS (k . 1)), the carrier of (REAL-NS (k . (n + 1)))) )
assume z in { F where F is Function of (REAL-NS (k . 1)),(REAL-NS (k . (n + 1))) : ex N being FinSequence st
( N is_Multilayer_perceptron_with k,n & F = OutPutFunc (N,k,n) ) } ; :: thesis: z in Funcs ( the carrier of (REAL-NS (k . 1)), the carrier of (REAL-NS (k . (n + 1))))
then ex F being Function of (REAL-NS (k . 1)),(REAL-NS (k . (n + 1))) st
( z = F & ex N being FinSequence st
( N is_Multilayer_perceptron_with k,n & F = OutPutFunc (N,k,n) ) ) ;
hence z in Funcs ( the carrier of (REAL-NS (k . 1)), the carrier of (REAL-NS (k . (n + 1)))) by FUNCT_2:8; :: thesis: verum

end;

hence { F where F is Function of (REAL-NS (k . 1)),(REAL-NS (k . (n + 1))) : ex N being FinSequence st
( N is_Multilayer_perceptron_with k,n & F = OutPutFunc (N,k,n) ) } is Subset of (Funcs ( the carrier of (REAL-NS (k . 1)), the carrier of (REAL-NS (k . (n + 1))))) by TARSKI:def 3; :: thesis: verum