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

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₁[ Nat] means ( 1 <= $1 & $1 <= len PF1 implies PF1 . $1 = PF2 . $1 );
A39: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A40: S₁[k] ; :: thesis: S₁[k + 1]

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

assume 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;

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

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

hence PF1 . (k + 1) = PF2 . (k + 1) by A34, A37; :: thesis: verum

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;

end;

end;

hence S₁[k + 1] ; :: thesis: verum

end;

A45: S₁[ 0 ] ;
for k being Nat holds S₁[k] from NAT_1:sch 2(A45, A39);
hence IT1 = IT2 by A32, A33, A36, FINSEQ_1:14; :: thesis: verum

end;

hence for b₁, b₂ being Function of E,E holds
( ( len F = 0 & b₁ = id E & b₂ = id E implies b₁ = b₂ ) & ( not len F = 0 & 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 ) ) ) & 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 ) ) ) implies b₁ = b₂ ) ) ; :: thesis: verum