per cases ;

suppose len F = 0 ; :: thesis:

hence ( ( len F = 0 implies ex b₁ being Function of E,E st b₁ = id E ) & ( not len F = 0 implies ex b₁ being Function of E,E ex PF being FinSequence of Funcs E,E st
( b₁ = PF . (len F) & len PF = len F & PF . 1 = A . (F . 1) & ( for n being Nat st n <> 0 & n < len F holds
ex f, g being Function of E,E st
( f = PF . n & g = A . (F . (n + 1)) & PF . (n + 1) = f * g ) ) ) ) ) ; :: thesis:

end;

suppose A1: len F <> 0 ; :: thesis:

defpred S₁[ Element of NAT ] means for F being FinSequence of O st len F = $1 & len F <> 0 holds
ex PF being FinSequence of Funcs E,E ex IT being Function of E,E st
( IT = PF . (len PF) & len PF = len F & PF . 1 = A . (F . 1) & ( for k being Nat st k <> 0 & k < len F holds
ex f, g being Function of E,E st
( f = PF . k & g = A . (F . (k + 1)) & PF . (k + 1) = f * g ) ) );
A2: S₁[ 0 ] ;
A3: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis:
assume A4: S₁[k] ; :: thesis:
thus S₁[k + 1] :: thesis:

proof

let F be FinSequence of O; :: thesis:
assume A5: ( len F = k + 1 & len F <> 0 ) ; :: thesis:
reconsider G = F | (Seg k) as FinSequence of O by FINSEQ_1:23;
A6: len G = k by A5, FINSEQ_3:59;

per cases ;

suppose A7: len G = 0 ; :: thesis:

set IT = A . (F . 1);
1 in Seg (len F) by A5, A6, A7;
then 1 in dom F by FINSEQ_1:def 3;
then F . 1 in rng F by FUNCT_1:12;
then F . 1 in O ;
then F . 1 in dom A by FUNCT_2:def 1;
then A . (F . 1) in rng A by FUNCT_1:12;
then reconsider IT = A . (F . 1) as Element of Funcs E,E ;
set PF = <*IT*>;
ex f being Function st
( IT = f & dom f = E & rng f c= E ) by FUNCT_2:def 2;
then reconsider IT = IT as Function of E,E by FUNCT_2:4;
take <*IT*> ; :: thesis:
take IT ; :: thesis:
( len <*IT*> = 1 & <*IT*> . 1 = IT ) by FINSEQ_1:57;
hence IT = <*IT*> . (len <*IT*>) ; :: thesis:
thus len <*IT*> = len F by A5, A6, A7, FINSEQ_1:57; :: thesis:
thus <*IT*> . 1 = A . (F . 1) by FINSEQ_1:57; :: thesis:
let k be Nat; :: thesis:
assume A8: ( k <> 0 & k < len F ) ; :: thesis:
consider f, g being Function of E,E;
take f ; :: thesis:
take g ; :: thesis:
thus ( f = <*IT*> . k & g = A . (F . (k + 1)) ) by A5, A6, A7, A8, NAT_1:14; :: thesis:
thus <*IT*> . (k + 1) = f * g by A5, A6, A7, A8, NAT_1:14; :: thesis:

end;

suppose A9: len G <> 0 ; :: thesis:

then consider PFk being FinSequence of Funcs E,E, ITk being Function of E,E such that
A10: ( ITk = PFk . (len PFk) & len PFk = len G & PFk . 1 = A . (G . 1) ) and
A11: for k being Nat st k <> 0 & k < len G holds
ex f, g being Function of E,E st
( f = PFk . k & g = A . (G . (k + 1)) & PFk . (k + 1) = f * g ) by A4, A6;
set f = PFk . k;
set g = A . (F . (k + 1));
0 < k by A6, A9;
then A12: 0 + 1 < k + 1 by XREAL_1:8;
then A13: 1 <= k by NAT_1:13;
then k in Seg (len PFk) by A6, A10;
then A14: k in dom PFk by FINSEQ_1:def 3;
then PFk . k in Funcs E,E by FINSEQ_2:13;
then ex f being Function st
( PFk . k = f & dom f = E & rng f c= E ) by FUNCT_2:def 2;
then reconsider f = PFk . k as Function of E,E by FUNCT_2:4;
k + 1 in Seg (len F) by A5, A12;
then k + 1 in dom F by FINSEQ_1:def 3;
then F . (k + 1) in rng F by FUNCT_1:12;
then F . (k + 1) in O ;
then F . (k + 1) in dom A by FUNCT_2:def 1;
then A . (F . (k + 1)) in rng A by FUNCT_1:12;
then ex f being Function st
( A . (F . (k + 1)) = f & dom f = E & rng f c= E ) by FUNCT_2:def 2;
then reconsider g = A . (F . (k + 1)) as Function of E,E by FUNCT_2:4;
set IT = f * g;
set PF = PFk ^ <*(f * g)*>;
f * g in Funcs E,E by FUNCT_2:12;
then <*(f * g)*> is FinSequence of Funcs E,E by FINSEQ_1:95;
then reconsider PF = PFk ^ <*(f * g)*> as FinSequence of Funcs E,E by FINSEQ_1:96;
A15: len PF = (len G) + (len <*(f * g)*>) by A10, FINSEQ_1:35
.= k + 1 by A6, FINSEQ_1:56 ;
then A16: len PF = (len PFk) + 1 by A5, A10, FINSEQ_3:59;
take PF ; :: thesis:
take f * g ; :: thesis:
thus A17: ( f * g = PF . (len PF) & len PF = len F ) by A5, A15, A16, FINSEQ_1:59; :: thesis:
0 < len G by A9;
then 0 + 1 < (len G) + 1 by XREAL_1:8;
then 1 <= len G by NAT_1:13;
then 1 in Seg (len PFk) by A10;
then 1 in dom PFk by FINSEQ_1:def 3;
then A18: PF . 1 = A . (G . 1) by A10, FINSEQ_1:def 7;
A19: 1 in Seg k by A13;
0 + k <= k + 1 by XREAL_1:8;
then 1 in (Seg (k + 1)) /\ (Seg k) by A19, FINSEQ_1:9;
then 1 in (dom F) /\ (Seg k) by A5, FINSEQ_1:def 3;
hence PF . 1 = A . (F . 1) by A18, FUNCT_1:71; :: thesis:
let n be Nat; :: thesis:
assume A20: n <> 0 ; :: thesis:
assume n < len F ; :: thesis:
then A21: n <= k by A5, NAT_1:13;

per cases ;

suppose A22: n >= k ; :: thesis:

then A23: n = k by A21, XXREAL_0:1;
A . (F . (n + 1)) = g by A21, A22, XXREAL_0:1;
then reconsider g' = A . (F . (n + 1)) as Function of E,E ;
reconsider f' = PF . n as Function of E,E by A14, A23, FINSEQ_1:def 7;
take f' ; :: thesis:
take g' ; :: thesis:
thus ( f' = PF . n & g' = A . (F . (n + 1)) ) ; :: thesis:
thus PF . (n + 1) = f' * g' by A14, A15, A17, A23, FINSEQ_1:def 7; :: thesis:

end;

suppose A24: n < k ; :: thesis:

then consider f', g' being Function of E,E such that
A25: ( f' = PFk . n & g' = A . (G . (n + 1)) & PFk . (n + 1) = f' * g' ) by A6, A11, A20;
0 < n by A20;
then A26: 0 + 1 < n + 1 by XREAL_1:8;
then ( 1 <= n & n <= k ) by A24, NAT_1:13;
then n in Seg (len PFk) by A6, A10, FINSEQ_1:3;
then A27: n in dom PFk by FINSEQ_1:def 3;
A28: ( 1 <= n + 1 & n + 1 <= k ) by A24, A26, NAT_1:13;
then n + 1 in Seg (len PFk) by A6, A10;
then A29: n + 1 in dom PFk by FINSEQ_1:def 3;
take f' ; :: thesis:
take g' ; :: thesis:
A30: n + 1 in Seg k by A28;
0 + k <= 1 + k by XREAL_1:8;
then n + 1 in (Seg (k + 1)) /\ (Seg k) by A30, FINSEQ_1:9;
then n + 1 in (dom F) /\ (Seg k) by A5, FINSEQ_1:def 3;
hence ( f' = PF . n & g' = A . (F . (n + 1)) ) by A25, A27, FINSEQ_1:def 7, FUNCT_1:71; :: thesis:
thus PF . (n + 1) = f' * g' by A25, A29, FINSEQ_1:def 7; :: thesis:

end;

A31: for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A2, A3);
ex PF being FinSequence of Funcs E,E ex IT being Function of E,E st
( IT = PF . (len PF) & len PF = len F & PF . 1 = A . (F . 1) & ( for k being Nat st k <> 0 & k < len F holds
ex f, g being Function of E,E st
( f = PF . k & g = A . (F . (k + 1)) & PF . (k + 1) = f * g ) ) ) by A1, A31;
hence ( ( len F = 0 implies ex b₁ being Function of E,E st b₁ = id E ) & ( not len F = 0 implies ex b₁ being Function of E,E ex PF being FinSequence of Funcs E,E st
( b₁ = PF . (len F) & len PF = len F & PF . 1 = A . (F . 1) & ( for n being Nat st n <> 0 & n < len F holds
ex f, g being Function of E,E st
( f = PF . n & g = A . (F . (n + 1)) & PF . (n + 1) = f * g ) ) ) ) ) ; :: thesis:

end;