theorem :: NEURONS1:30

for N being Multilayer_perceptron ex k being FinSequence of NAT st
( (len N) + 1 = len k & ( for i being Nat st 1 <= i & i < len k holds
N . i is Function of (REAL-NS (k . i)),(REAL-NS (k . (i + 1))) ) ) by Def2;