now :: thesis: for IT1, IT2 being Function of E,E st ex PF1 being FinSequence of Funcs (E,E) st

( IT1 = PF1 . (len F) & len PF1 = len F & PF1 . 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 = PF1 . k & g = A . (F . (k + 1)) & PF1 . (k + 1) = f * g ) ) ) & ex PF2 being FinSequence of Funcs (E,E) st

( IT2 = PF2 . (len F) & len PF2 = len F & PF2 . 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 = PF2 . k & g = A . (F . (k + 1)) & PF2 . (k + 1) = f * g ) ) ) holds

IT1 = IT2

hence
for b( IT1 = PF1 . (len F) & len PF1 = len F & PF1 . 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 = PF1 . k & g = A . (F . (k + 1)) & PF1 . (k + 1) = f * g ) ) ) & ex PF2 being FinSequence of Funcs (E,E) st

( IT2 = PF2 . (len F) & len PF2 = len F & PF2 . 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 = PF2 . k & g = A . (F . (k + 1)) & PF2 . (k + 1) = f * g ) ) ) holds

IT1 = IT2

let IT1, IT2 be Function of E,E; :: thesis: ( ex PF1 being FinSequence of Funcs (E,E) st

( IT1 = PF1 . (len F) & len PF1 = len F & PF1 . 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 = PF1 . k & g = A . (F . (k + 1)) & PF1 . (k + 1) = f * g ) ) ) & ex PF2 being FinSequence of Funcs (E,E) st

( IT2 = PF2 . (len F) & len PF2 = len F & PF2 . 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 = PF2 . k & g = A . (F . (k + 1)) & PF2 . (k + 1) = f * g ) ) ) implies IT1 = IT2 )

given PF1 being FinSequence of Funcs (E,E) such that A32: IT1 = PF1 . (len F) and

A33: len PF1 = len F and

A34: PF1 . 1 = A . (F . 1) and

A35: for k being Nat st k <> 0 & k < len F holds

ex f, g being Function of E,E st

( f = PF1 . k & g = A . (F . (k + 1)) & PF1 . (k + 1) = f * g ) ; :: thesis: ( ex PF2 being FinSequence of Funcs (E,E) st

( IT2 = PF2 . (len F) & len PF2 = len F & PF2 . 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 = PF2 . k & g = A . (F . (k + 1)) & PF2 . (k + 1) = f * g ) ) ) implies IT1 = IT2 )

given PF2 being FinSequence of Funcs (E,E) such that A36: ( IT2 = PF2 . (len F) & len PF2 = len F ) and

A37: PF2 . 1 = A . (F . 1) and

A38: for k being Nat st k <> 0 & k < len F holds

ex f, g being Function of E,E st

( f = PF2 . k & g = A . (F . (k + 1)) & PF2 . (k + 1) = f * g ) ; :: thesis: IT1 = IT2

defpred S_{1}[ Nat] means ( 1 <= $1 & $1 <= len PF1 implies PF1 . $1 = PF2 . $1 );

A39: 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(A45, A39);

hence IT1 = IT2 by A32, A33, A36, FINSEQ_1:14; :: thesis: verum

end;( IT1 = PF1 . (len F) & len PF1 = len F & PF1 . 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 = PF1 . k & g = A . (F . (k + 1)) & PF1 . (k + 1) = f * g ) ) ) & ex PF2 being FinSequence of Funcs (E,E) st

( IT2 = PF2 . (len F) & len PF2 = len F & PF2 . 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 = PF2 . k & g = A . (F . (k + 1)) & PF2 . (k + 1) = f * g ) ) ) implies IT1 = IT2 )

given PF1 being FinSequence of Funcs (E,E) such that A32: IT1 = PF1 . (len F) and

A33: len PF1 = len F and

A34: PF1 . 1 = A . (F . 1) and

A35: for k being Nat st k <> 0 & k < len F holds

ex f, g being Function of E,E st

( f = PF1 . k & g = A . (F . (k + 1)) & PF1 . (k + 1) = f * g ) ; :: thesis: ( ex PF2 being FinSequence of Funcs (E,E) st

( IT2 = PF2 . (len F) & len PF2 = len F & PF2 . 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 = PF2 . k & g = A . (F . (k + 1)) & PF2 . (k + 1) = f * g ) ) ) implies IT1 = IT2 )

given PF2 being FinSequence of Funcs (E,E) such that A36: ( IT2 = PF2 . (len F) & len PF2 = len F ) and

A37: PF2 . 1 = A . (F . 1) and

A38: for k being Nat st k <> 0 & k < len F holds

ex f, g being Function of E,E st

( f = PF2 . k & g = A . (F . (k + 1)) & PF2 . (k + 1) = f * g ) ; :: thesis: IT1 = IT2

defpred S

A39: for k being Nat st S

S

proof

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

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

_{1}[k + 1]
; :: thesis: verum

end;assume A40: S

now :: thesis: ( 1 <= k + 1 & k + 1 <= len PF1 implies PF1 . (k + 1) = PF2 . (k + 1) )

hence
Sassume
1 <= k + 1
; :: thesis: ( k + 1 <= len PF1 implies PF1 . (k + 1) = PF2 . (k + 1) )

assume A41: k + 1 <= len PF1 ; :: thesis: PF1 . (k + 1) = PF2 . (k + 1)

then A42: k < len PF1 by NAT_1:13;

end;assume A41: k + 1 <= len PF1 ; :: thesis: PF1 . (k + 1) = PF2 . (k + 1)

then A42: k < len PF1 by NAT_1:13;

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

end;

suppose A43:
k <> 0
; :: thesis: PF1 . (k + 1) = PF2 . (k + 1)

then A44:
0 + 1 < k + 1
by XREAL_1:6;

( ex f1, g1 being Function of E,E st

( f1 = PF1 . k & g1 = A . (F . (k + 1)) & PF1 . (k + 1) = f1 * g1 ) & ex f2, g2 being Function of E,E st

( f2 = PF2 . k & g2 = A . (F . (k + 1)) & PF2 . (k + 1) = f2 * g2 ) ) by A33, A35, A38, A42, A43;

hence PF1 . (k + 1) = PF2 . (k + 1) by A40, A41, A44, NAT_1:13; :: thesis: verum

end;( ex f1, g1 being Function of E,E st

( f1 = PF1 . k & g1 = A . (F . (k + 1)) & PF1 . (k + 1) = f1 * g1 ) & ex f2, g2 being Function of E,E st

( f2 = PF2 . k & g2 = A . (F . (k + 1)) & PF2 . (k + 1) = f2 * g2 ) ) by A33, A35, A38, A42, A43;

hence PF1 . (k + 1) = PF2 . (k + 1) by A40, A41, A44, NAT_1:13; :: thesis: verum

for k being Nat holds S

hence IT1 = IT2 by A32, A33, A36, FINSEQ_1:14; :: thesis: verum

( ( len F = 0 & b

( b

ex f, g being Function of E,E st

( f = PF . n & g = A . (F . (n + 1)) & PF . (n + 1) = f * g ) ) ) & ex PF being FinSequence of Funcs (E,E) st

( b

ex f, g being Function of E,E st

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