:: deftheorem Def3 defines OutPutFunc NEURONS1:def 3 :
for n being Nat
for k being FinSequence of NAT
for N being FinSequence st N is_Multilayer_perceptron_with k,n & len N <> 0 holds
for b4 being Function of (REAL-NS (k . 1)),(REAL-NS (k . (n + 1))) holds
( b4 = OutPutFunc (N,k,n) iff ex p being FinSequence st
( len p = len N & p . 1 = N . 1 & ( for i being Nat st 1 <= i & i < len N holds
ex NN being Function of (REAL-NS (k . (i + 1))),(REAL-NS (k . (i + 2))) ex pp being Function of (REAL-NS (k . 1)),(REAL-NS (k . (i + 1))) st
( NN = N . (i + 1) & pp = p . i & p . (i + 1) = NN * pp ) ) & b4 = p . (len N) ) );