:: deftheorem defines is_LayerFunc_Seq NEURONS1:def 6 :
for n being Nat
for k being FinSequence of NAT
for D, K being Real
for N being FinSequence holds
( N is_LayerFunc_Seq D,K,k,n iff ( len N = n & N is_Multilayer_perceptron_with k,n & ( for i being Nat st 1 <= i & i < len k holds
ex Ni being Function of (REAL-NS (k . i)),(REAL-NS (k . (i + 1))) st
( N . i = Ni & Ni is_LayerFunc D,K ) ) ) );