:: deftheorem defines NEURONS NEURONS1:def 4 :
for n being Nat
for k being FinSequence of NAT holds NEURONS (n,k) = { 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) )
}
;