consider N being FinSequence such that
A1: 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 Lm1;
take N ; :: thesis: N is Multilayer_perceptron_like
thus N is Multilayer_perceptron_like by A1; :: thesis: verum