let n be Nat; :: thesis: 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)) )
let k be FinSequence of NAT ; :: thesis: 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)) )
let N be non empty FinSequence; :: thesis: ( n <> 0 & N is_Multilayer_perceptron_with k,n + 1 implies 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)) ) )
assume A1: n <> 0 ; :: thesis: ( not N is_Multilayer_perceptron_with k,n + 1 or 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)) ) )
assume A2: N is_Multilayer_perceptron_with k,n + 1 ; :: thesis: 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)) )
then A3: len (N | n) = n by FINSEQ_1:59, NAT_1:11;
reconsider N1 = N | n as non empty FinSequence by A1;
reconsider k1 = k | (n + 1) as FinSequence of NAT ;
for i being Nat st 1 <= i & i < len k1 holds
N1 . i is Function of (REAL-NS (k1 . i)),(REAL-NS (k1 . (i + 1)))

proof

let i be Nat; :: thesis: ( 1 <= i & i < len k1 implies N1 . i is Function of (REAL-NS (k1 . i)),(REAL-NS (k1 . (i + 1))) )
assume A4: ( 1 <= i & i < len k1 ) ; :: thesis: N1 . i is Function of (REAL-NS (k1 . i)),(REAL-NS (k1 . (i + 1)))
A5: len k1 = n + 1 by A2, FINSEQ_1:59, NAT_1:11;
then len k1 <= len k by NAT_1:11, A2;
then i < len k by A4, XXREAL_0:2;
then A7: N . i is Function of (REAL-NS (k . i)),(REAL-NS (k . (i + 1))) by A2, A4;
i in Seg (n + 1) by A4, A5;
then A8: k1 . i = k . i by FUNCT_1:49;
A9: i + 1 <= len k1 by NAT_1:13, A4;
1 <= i + 1 by NAT_1:11;
then i + 1 in Seg (n + 1) by A5, A9;
then A10: k1 . (i + 1) = k . (i + 1) by FUNCT_1:49;
i <= n by A4, A5, NAT_1:13;
then i in Seg n by A4;
hence N1 . i is Function of (REAL-NS (k1 . i)),(REAL-NS (k1 . (i + 1))) by A7, A8, A10, FUNCT_1:49; :: thesis: verum

end;

then A11: N1 is_Multilayer_perceptron_with k1,n by A2, FINSEQ_1:59, NAT_1:11, A3;
consider p being FinSequence such that
A12: ( 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 ) ) & OutPutFunc (N,k,(n + 1)) = p . (len N) ) by Def3, A2;
set p1 = p | n;
A13: 1 <= n by A1, NAT_1:14;
then A14: 1 in Seg n ;
then A15: (p | n) . 1 = p . 1 by FUNCT_1:49
.= N1 . 1 by FUNCT_1:49, A14, A12 ;
A16: len (p | n) = n by A2, A12, FINSEQ_1:59, NAT_1:11
.= len N1 by A2, FINSEQ_1:59, NAT_1:11 ;

A17: now :: thesis: for i being Nat st 1 <= i & i < len N1 holds
ex NN being Function of (REAL-NS (k1 . (i + 1))),(REAL-NS (k1 . (i + 2))) ex pp being Function of (REAL-NS (k1 . 1)),(REAL-NS (k1 . (i + 1))) st
( NN = N1 . (i + 1) & pp = (p | n) . i & (p | n) . (i + 1) = NN * pp )

let i be Nat; :: thesis: ( 1 <= i & i < len N1 implies ex NN being Function of (REAL-NS (k1 . (i + 1))),(REAL-NS (k1 . (i + 2))) ex pp being Function of (REAL-NS (k1 . 1)),(REAL-NS (k1 . (i + 1))) st
( NN = N1 . (i + 1) & pp = (p | n) . i & (p | n) . (i + 1) = NN * pp ) )
assume A18: ( 1 <= i & i < len N1 ) ; :: thesis: ex NN being Function of (REAL-NS (k1 . (i + 1))),(REAL-NS (k1 . (i + 2))) ex pp being Function of (REAL-NS (k1 . 1)),(REAL-NS (k1 . (i + 1))) st
( NN = N1 . (i + 1) & pp = (p | n) . i & (p | n) . (i + 1) = NN * pp )
A19: len N1 = n by A2, FINSEQ_1:59, NAT_1:11;
then A20: len N1 <= len N by A2, NAT_1:11;
then i < len N by A18, XXREAL_0:2;
then consider NN being Function of (REAL-NS (k . (i + 1))),(REAL-NS (k . (i + 2))), pp being Function of (REAL-NS (k . 1)),(REAL-NS (k . (i + 1))) such that
A21: ( NN = N . (i + 1) & pp = p . i & p . (i + 1) = NN * pp ) by A18, A12;
i in Seg n by A18, A19;
then A22: (p | n) . i = p . i by FUNCT_1:49;
A23: i + 1 <= len N1 by NAT_1:13, A18;
A24: 1 <= i + 1 by NAT_1:11;
then A25: i + 1 in Seg n by A19, A23;
then A26: N1 . (i + 1) = N . (i + 1) by FUNCT_1:49;
A27: (p | n) . (i + 1) = p . (i + 1) by FUNCT_1:49, A25;
i + 1 <= n + 1 by A2, A20, A23, XXREAL_0:2;
then i + 1 in Seg (n + 1) by A24;
then A28: k1 . (i + 1) = k . (i + 1) by FUNCT_1:49;
( 1 <= 1 & 1 <= n + 1 ) by NAT_1:11;
then 1 in Seg (n + 1) ;
then A29: k1 . 1 = k . 1 by FUNCT_1:49;
A30: (i + 1) + 1 <= (len N1) + 1 by A23, XREAL_1:7;
1 <= (i + 1) + 1 by NAT_1:11;
then (i + 1) + 1 in Seg (n + 1) by A19, A30;
then k1 . (i + 2) = k . (i + 2) by FUNCT_1:49;
hence ex NN being Function of (REAL-NS (k1 . (i + 1))),(REAL-NS (k1 . (i + 2))) ex pp being Function of (REAL-NS (k1 . 1)),(REAL-NS (k1 . (i + 1))) st
( NN = N1 . (i + 1) & pp = (p | n) . i & (p | n) . (i + 1) = NN * pp ) by A21, A22, A26, A27, A28, A29; :: thesis: verum

end;

A32: n in Seg n by A13;
n + 0 < n + 1 by XREAL_1:8;
then consider NN being Function of (REAL-NS (k . (n + 1))),(REAL-NS (k . (n + 2))), pp being Function of (REAL-NS (k . 1)),(REAL-NS (k . (n + 1))) such that
A33: ( NN = N . (n + 1) & pp = p . n & p . (n + 1) = NN * pp ) by A1, A2, A12, NAT_1:14;
A34: pp = (p | n) . (len N1) by A3, A32, A33, FUNCT_1:49;
( 1 <= 1 & 1 <= n + 1 ) by NAT_1:11;
then 1 in Seg (n + 1) ;
then A35: k1 . 1 = k . 1 by FUNCT_1:49;
A36: k1 . (n + 1) = k . (n + 1) by FUNCT_1:49, FINSEQ_1:4;
take k1 ; :: thesis: 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)) )
take N1 ; :: thesis: 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)) )
take NN ; :: thesis: ( 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)) )
thus ( N1 = N | n & k1 = k | (n + 1) & NN = N . (n + 1) ) by A33; :: thesis: ( N1 is_Multilayer_perceptron_with k1,n & OutPutFunc (N,k,(n + 1)) = NN * (OutPutFunc (N1,k1,n)) )
thus N1 is_Multilayer_perceptron_with k1,n by A11; :: thesis: OutPutFunc (N,k,(n + 1)) = NN * (OutPutFunc (N1,k1,n))
thus OutPutFunc (N,k,(n + 1)) = NN * (OutPutFunc (N1,k1,n)) by A11, A15, A16, A17, A33, A34, A35, A36, Def3, A2, A12; :: thesis: verum