theorem Th34: :: NEURONS1:34

for D, K being Real st 0 <= D & 0 <= K holds
for n being Nat
for k being FinSequence of NAT
for N being non empty FinSequence st N is_LayerFunc_Seq D,K,k,n holds
OutPutFunc (N,k,n) is_LayerFunc D |^ n,K