theorem Th31: :: NEURONS1:31

for n being Nat
for k being FinSequence of NAT
for N being non empty FinSequence st n <> 0 & N is_Multilayer_perceptron_with k,n + 1 holds
ex k1 being FinSequence of NAT ex N1 being non empty FinSequence ex NN being Function of (REAL-NS (k . (n + 1))),(REAL-NS (k . (n + 2))) st
( N1 = N | n & k1 = k | (n + 1) & NN = N . (n + 1) & N1 is_Multilayer_perceptron_with k1,n & OutPutFunc (N,k,(n + 1)) = NN * (OutPutFunc (N1,k1,n)) )