per cases
( len F = 0 or len F <> 0 )
;

end;

suppose
len F = 0
; :: thesis: ( ( len F = 0 implies ex b_{1} being Function of E,E st b_{1} = id E ) & ( not len F = 0 implies ex b_{1} being Function of E,E ex PF being FinSequence of Funcs (E,E) st

( b_{1} = 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 ) ) ) ) )

( b

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 b_{1} being Function of E,E st b_{1} = id E ) & ( not len F = 0 implies ex b_{1} being Function of E,E ex PF being FinSequence of Funcs (E,E) st

( b_{1} = 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;( b

ex f, g being Function of E,E st

( f = PF . n & g = A . (F . (n + 1)) & PF . (n + 1) = f * g ) ) ) ) ) ; :: thesis: verum

suppose A1:
len F <> 0
; :: thesis: ( ( len F = 0 implies ex b_{1} being Function of E,E st b_{1} = id E ) & ( not len F = 0 implies ex b_{1} being Function of E,E ex PF being FinSequence of Funcs (E,E) st

( b_{1} = 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 ) ) ) ) )

( b

ex f, g being Function of E,E st

( f = PF . n & g = A . (F . (n + 1)) & PF . (n + 1) = f * g ) ) ) ) )

defpred S_{1}[ 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_{1}[k] holds

S_{1}[k + 1]
_{1}[ 0 ]
;

for k being Nat holds S_{1}[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_{1} being Function of E,E st b_{1} = id E ) & ( not len F = 0 implies ex b_{1} being Function of E,E ex PF being FinSequence of Funcs (E,E) st

( b_{1} = 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;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

S

proof

A31:
S
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A3: S_{1}[k]
; :: thesis: S_{1}[k + 1]

thus S_{1}[k + 1]
:: thesis: verum

end;assume A3: S

thus S

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 A4, FINSEQ_3:53;

end;( 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 A4, FINSEQ_3:53;

per cases
( len G = 0 or len G <> 0 )
;

end;

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 ) ) )

( 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 A4, A5, A6, FINSEQ_1:40; :: 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;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 A4, A5, A6, FINSEQ_1:40; :: 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

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 ) ) )

( 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 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: 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 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: ( 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 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: 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 A4, NAT_1:13;

end;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: 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 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: ( 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 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: 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 A4, NAT_1:13;

per cases
( n >= k or n < k )
;

end;

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 )

( f = PF . n & g = A . (F . (n + 1)) & PF . (n + 1) = f * g )

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: 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 A17, A18, A19, A23, FINSEQ_1:def 7; :: thesis: verum

end;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: 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 A17, A18, A19, A23, FINSEQ_1:def 7; :: thesis: verum

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 )

( f = PF . n & g = A . (F . (n + 1)) & PF . (n + 1) = f * g )

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: 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 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: 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 A28, FINSEQ_1:def 7; :: thesis: verum

end;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 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: 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 A28, FINSEQ_1:def 7; :: thesis: verum

for k being Nat holds S

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

( b

ex f, g being Function of E,E st

( f = PF . n & g = A . (F . (n + 1)) & PF . (n + 1) = f * g ) ) ) ) ) ; :: thesis: verum