per cases ( len F = 0 or len F <> 0 ) ;
suppose len F = 0 ; :: thesis: ( ( len F = 0 implies ex b1 being Function of E,E st b1 = id E ) & ( not len F = 0 implies ex b1 being Function of E,E ex PF being FinSequence of Funcs (E,E) st
( b1 = 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 ) ) ) ) )

hence ( ( len F = 0 implies ex b1 being Function of E,E st b1 = id E ) & ( not len F = 0 implies ex b1 being Function of E,E ex PF being FinSequence of Funcs (E,E) st
( b1 = 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: verum
end;
suppose A1: len F <> 0 ; :: thesis: ( ( len F = 0 implies ex b1 being Function of E,E st b1 = id E ) & ( not len F = 0 implies ex b1 being Function of E,E ex PF being FinSequence of Funcs (E,E) st
( b1 = 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 ) ) ) ) )

defpred S1[ 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 S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A3: S1[k] ; :: thesis: S1[k + 1]
thus S1[k + 1] :: thesis: verum
proof
let F be FinSequence of O; :: thesis: ( len F = k + 1 & len F <> 0 implies 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 ) ) ) )

assume that
A4: len F = k + 1 and
len F <> 0 ; :: thesis: 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 ) ) )

reconsider G = F | (Seg k) as FinSequence of O by FINSEQ_1:18;
A5: len G = k by ;
per cases ( len G = 0 or len G <> 0 ) ;
suppose A6: len G = 0 ; :: thesis: 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 ) ) )

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: ex IT being Function of E,E st
( IT = <*IT*> . (len <*IT*>) & len <*IT*> = len F & <*IT*> . 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 = <*IT*> . k & g = A . (F . (k + 1)) & <*IT*> . (k + 1) = f * g ) ) )

take IT ; :: thesis: ( IT = <*IT*> . (len <*IT*>) & len <*IT*> = len F & <*IT*> . 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 = <*IT*> . k & g = A . (F . (k + 1)) & <*IT*> . (k + 1) = f * g ) ) )

len <*IT*> = 1 by FINSEQ_1:40;
hence IT = <*IT*> . (len <*IT*>) by FINSEQ_1:40; :: thesis: ( len <*IT*> = len F & <*IT*> . 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 = <*IT*> . k & g = A . (F . (k + 1)) & <*IT*> . (k + 1) = f * g ) ) )

thus len <*IT*> = len F by ; :: thesis: ( <*IT*> . 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 = <*IT*> . k & g = A . (F . (k + 1)) & <*IT*> . (k + 1) = f * g ) ) )

thus <*IT*> . 1 = A . (F . 1) by FINSEQ_1:40; :: thesis: for k being Nat st k <> 0 & k < len F holds
ex f, g being Function of E,E st
( f = <*IT*> . k & g = A . (F . (k + 1)) & <*IT*> . (k + 1) = f * g )

let k be Nat; :: thesis: ( k <> 0 & k < len F implies ex f, g being Function of E,E st
( f = <*IT*> . k & g = A . (F . (k + 1)) & <*IT*> . (k + 1) = f * g ) )

assume A8: ( k <> 0 & k < len F ) ; :: thesis: ex f, g being Function of E,E st
( f = <*IT*> . k & g = A . (F . (k + 1)) & <*IT*> . (k + 1) = f * g )

take the Function of E,E ; :: thesis: ex g being Function of E,E st
( the Function of E,E = <*IT*> . k & g = A . (F . (k + 1)) & <*IT*> . (k + 1) = the Function of E,E * g )

take the Function of E,E ; :: thesis: ( the Function of E,E = <*IT*> . k & the Function of E,E = A . (F . (k + 1)) & <*IT*> . (k + 1) = the Function of E,E * the Function of E,E )
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: <*IT*> . (k + 1) = the Function of E,E * the Function of E,E
thus <*IT*> . (k + 1) = the Function of E,E * the Function of E,E by A4, A5, A6, A8, NAT_1:14; :: thesis: verum
end;
suppose A9: len G <> 0 ; :: thesis: 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 ) ) )

set g = A . (F . (k + 1));
A10: 0 + k <= k + 1 by XREAL_1:6;
A11: 0 + 1 < k + 1 by ;
then A12: 1 <= k by NAT_1:13;
then 1 in Seg k ;
then 1 in (Seg (k + 1)) /\ (Seg k) by ;
then A13: 1 in (dom F) /\ (Seg k) by ;
k + 1 in Seg (len F) by ;
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 ;
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: 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 ) ) )

take f * g ; :: thesis: ( f * g = 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 ) ) )

A18: len PF = (len G) + (len <*(f * g)*>) by
.= k + 1 by ;
then len PF = (len PFk) + 1 by ;
hence A19: ( f * g = PF . (len PF) & len PF = len F ) by ; :: thesis: ( 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 ) ) )

0 + 1 < (len G) + 1 by ;
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 ;
hence PF . 1 = A . (F . 1) by ; :: thesis: 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 )

let n be Nat; :: thesis: ( n <> 0 & n < len F implies ex f, g being Function of E,E st
( f = PF . n & g = A . (F . (n + 1)) & PF . (n + 1) = f * g ) )

assume A20: n <> 0 ; :: thesis: ( not n < len F or ex f, g being Function of E,E st
( f = PF . n & g = A . (F . (n + 1)) & PF . (n + 1) = f * g ) )

assume n < len F ; :: thesis: ex f, g being Function of E,E st
( f = PF . n & g = A . (F . (n + 1)) & PF . (n + 1) = f * g )

then A21: n <= k by ;
per cases ( n >= k or n < k ) ;
suppose A22: n >= k ; :: thesis: ex f, g being Function of E,E st
( f = PF . n & g = A . (F . (n + 1)) & PF . (n + 1) = f * g )

then A . (F . (n + 1)) = g by ;
then reconsider g9 = A . (F . (n + 1)) as Function of E,E ;
A23: n = k by ;
then reconsider f9 = PF . n as Function of E,E by ;
take f9 ; :: thesis: ex g being Function of E,E st
( f9 = PF . n & g = A . (F . (n + 1)) & PF . (n + 1) = f9 * g )

take g9 ; :: thesis: ( f9 = PF . n & g9 = A . (F . (n + 1)) & PF . (n + 1) = f9 * g9 )
thus ( f9 = PF . n & g9 = A . (F . (n + 1)) ) ; :: thesis: PF . (n + 1) = f9 * g9
thus PF . (n + 1) = f9 * g9 by ; :: thesis: verum
end;
suppose A24: n < k ; :: thesis: ex f, g being Function of E,E st
( f = PF . n & g = A . (F . (n + 1)) & PF . (n + 1) = f * g )

A25: 0 + 1 < n + 1 by ;
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: ex g being Function of E,E st
( f9 = PF . n & g = A . (F . (n + 1)) & PF . (n + 1) = f9 * g )

take g9 ; :: thesis: ( f9 = PF . n & g9 = A . (F . (n + 1)) & PF . (n + 1) = f9 * g9 )
A29: 0 + k <= 1 + k by XREAL_1:6;
A30: n + 1 <= k by ;
then n + 1 in Seg k by A25;
then n + 1 in (Seg (k + 1)) /\ (Seg k) by ;
then n + 1 in (dom F) /\ (Seg k) by ;
hence ( f9 = PF . n & g9 = A . (F . (n + 1)) ) by ; :: thesis: PF . (n + 1) = f9 * g9
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 ; :: thesis: verum
end;
end;
end;
end;
end;
end;
A31: S1[ 0 ] ;
for k being Nat holds S1[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 b1 being Function of E,E st b1 = id E ) & ( not len F = 0 implies ex b1 being Function of E,E ex PF being FinSequence of Funcs (E,E) st
( b1 = 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: verum
end;
end;