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₁[ 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: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis:
assume A3: S₁[k] ; :: thesis:
thus S₁[k + 1] :: thesis:

proof

let F be FinSequence of O; :: thesis:
assume that
A4: len F = k + 1 and
len F <> 0 ; :: thesis:
reconsider G = F | (Seg k) as FinSequence of O by FINSEQ_1:18;
A5: len G = k by A4, FINSEQ_3:53;

per cases ;

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

set IT = A . (F . 1);
1 in Seg (len F) by A4, A5, A6;
then 1 in dom F by FINSEQ_1:def 3;
then F . 1 in rng F by FUNCT_1:3;
then F . 1 in O ;
then F . 1 in dom A by FUNCT_2:def 1;
then A7: A . (F . 1) in rng A by FUNCT_1:3;
set f = the Function of E,E;
reconsider IT = A . (F . 1) as Element of Funcs (E,E) by A7;
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:2;
take <*IT*> ; :: thesis:
take IT ; :: thesis:
len <*IT*> = 1 by FINSEQ_1:40;
hence IT = <*IT*> . (len <*IT*>) ; :: thesis:
thus len <*IT*> = len F by A4, A5, A6, FINSEQ_1:40; :: thesis:
thus <*IT*> . 1 = A . (F . 1) ; :: thesis:
let k be Nat; :: thesis:
assume A8: ( k <> 0 & k < len F ) ; :: thesis:
take the Function of E,E ; :: thesis:
take the Function of E,E ; :: thesis:
thus ( the Function of E,E = <*IT*> . k & the Function of E,E = A . (F . (k + 1)) ) by A4, A5, A6, A8, NAT_1:14; :: thesis:
thus <*IT*> . (k + 1) = the Function of E,E * the Function of E,E by A4, A5, A6, A8, NAT_1:14; :: thesis:

end;

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

set g = A . (F . (k + 1));
A10: 0 + k <= k + 1 by XREAL_1:6;
A11: 0 + 1 < k + 1 by A5, A9, XREAL_1:6;
then A12: 1 <= k by NAT_1:13;
then 1 in Seg k ;
then 1 in (Seg (k + 1)) /\ (Seg k) by A10, FINSEQ_1:7;
then A13: 1 in (dom F) /\ (Seg k) by A4, FINSEQ_1:def 3;
k + 1 in Seg (len F) by A4, A11;
then k + 1 in dom F by FINSEQ_1:def 3;
then F . (k + 1) in rng F by FUNCT_1:3;
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:3;
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:2;
consider PFk being FinSequence of Funcs (E,E), ITk being Function of E,E such that
ITk = PFk . (len PFk) and
A14: len PFk = len G and
A15: PFk . 1 = A . (G . 1) and
A16: 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 A3, A4, A9, FINSEQ_3:53;
set f = PFk . k;
k in Seg (len PFk) by A5, A14, A12;
then A17: k in dom PFk by FINSEQ_1:def 3;
then PFk . k in Funcs (E,E) by FINSEQ_2:11;
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:2;
set IT = f * g;
set PF = PFk ^ <*(f * g)*>;
f * g in Funcs (E,E) by FUNCT_2:9;
then <*(f * g)*> is FinSequence of Funcs (E,E) by FINSEQ_1:74;
then reconsider PF = PFk ^ <*(f * g)*> as FinSequence of Funcs (E,E) by FINSEQ_1:75;
take PF ; :: thesis:
take f * g ; :: thesis:
A18: len PF = (len G) + (len <*(f * g)*>) by A14, FINSEQ_1:22
.= k + 1 by A5, FINSEQ_1:39 ;
then len PF = (len PFk) + 1 by A4, A14, FINSEQ_3:53;
hence A19: ( f * g = PF . (len PF) & len PF = len F ) by A4, A18, FINSEQ_1:42; :: thesis:
0 + 1 < (len G) + 1 by A9, XREAL_1:6;
then 1 <= len G by NAT_1:13;
then 1 in Seg (len PFk) by A14;
then 1 in dom PFk by FINSEQ_1:def 3;
then PF . 1 = A . (G . 1) by A15, FINSEQ_1:def 7;
hence PF . 1 = A . (F . 1) by A13, FUNCT_1:48; :: thesis:
let n be Nat; :: thesis:
assume A20: n <> 0 ; :: thesis:
assume n < len F ; :: thesis:
then A21: n <= k by A4, NAT_1:13;

per cases ;

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

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

end;

suppose A24: n < k ; :: thesis:

A25: 0 + 1 < n + 1 by A20, XREAL_1:6;
then 1 <= n by NAT_1:13;
then n in Seg (len PFk) by A5, A14, A24;
then A26: n in dom PFk by FINSEQ_1:def 3;
consider f9, g9 being Function of E,E such that
A27: ( f9 = PFk . n & g9 = A . (G . (n + 1)) ) and
A28: PFk . (n + 1) = f9 * g9 by A5, A16, A20, A24;
take f9 ; :: thesis:
take g9 ; :: thesis:
A29: 0 + k <= 1 + k by XREAL_1:6;
A30: n + 1 <= k by A24, NAT_1:13;
then n + 1 in Seg k by A25;
then n + 1 in (Seg (k + 1)) /\ (Seg k) by A29, FINSEQ_1:7;
then n + 1 in (dom F) /\ (Seg k) by A4, FINSEQ_1:def 3;
hence ( f9 = PF . n & g9 = A . (F . (n + 1)) ) by A27, A26, FINSEQ_1:def 7, FUNCT_1:48; :: thesis:
n + 1 in Seg (len PFk) by A5, A14, A25, A30;
then n + 1 in dom PFk by FINSEQ_1:def 3;
hence PF . (n + 1) = f9 * g9 by A28, FINSEQ_1:def 7; :: thesis:

end;

A31: S₁[ 0 ] ;
for k being Nat holds S₁[k] from NAT_1:sch 2(A31, A2);
then 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;
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;